conjure_core/solver/adaptors/rustsat/
convs.rs

Help
1use std::{collections::HashMap, env::Vars, io::Lines};
2
3use rustsat::{
4    clause,
5    instances::{BasicVarManager, Cnf, SatInstance},
6    solvers::{Solve, SolverResult},
7    types::{Lit, TernaryVal},
8};
9
10use rustsat_minisat::core::Minisat;
11
12use anyhow::{anyhow, Result};
13
14use crate::{ast::Expression, solver::Error};
15
16pub fn handle_lit(
17    l1: &Expression,
18    vars_added: &mut HashMap<String, Lit>,
19    inst: &mut SatInstance,
20) -> Lit {
21    match l1 {
22        // simple literal
23        // TODO (ss504) check what can be done to avoid cloning
24        Expression::Atomic(_, _) => handle_atom(l1.clone(), true, vars_added, inst),
25        // not literal
26        Expression::Not(_, _) => handle_not(l1, vars_added, inst),
27
28        _ => panic!("Literal expected"),
29    }
30}
31
32pub fn handle_not(
33    expr: &Expression,
34    vars_added: &mut HashMap<String, Lit>,
35    inst: &mut SatInstance,
36) -> Lit {
37    match expr {
38        Expression::Not(_, ref_heap_a) => {
39            // TODO (ss504) check what can be done to avoid cloning
40            let a = ref_heap_a.clone();
41            // and then unbox
42            handle_atom(*a, false, vars_added, inst)
43        }
44        _ => panic!("Not Expected"),
45    }
46}
47
48pub fn handle_atom(
49    a: Expression,
50    polarity: bool,
51    vars_added: &mut HashMap<String, Lit>,
52    inst: &mut SatInstance,
53) -> Lit {
54    // polarity false for not
55    match a {
56        Expression::Atomic(_, atom) => match atom {
57            conjure_core::ast::Atom::Literal(literal) => {
58                todo!("Not Sure if we are handling Lits as-is or not..")
59            }
60            conjure_core::ast::Atom::Reference(name) => match name {
61                conjure_core::ast::Name::UserName(n) => {
62                    // TODO: Temp Clone
63                    // let m = n.clone();
64                    let lit_temp: Lit = fetch_lit(n, vars_added, inst);
65                    if polarity {
66                        lit_temp
67                    } else {
68                        !lit_temp
69                    }
70                }
71                _ => {
72                    todo!("Change Here for other types of vars")
73                }
74            },
75        },
76        _ => panic!("atomic expected"),
77    }
78}
79
80pub fn fetch_lit(
81    symbol: String,
82    vars_added: &mut HashMap<String, Lit>,
83    inst: &mut SatInstance,
84) -> Lit {
85    if !vars_added.contains_key(&symbol) {
86        vars_added.insert(symbol.to_string(), inst.new_lit());
87    }
88    *(vars_added.get(&symbol).unwrap())
89}
90
91pub fn handle_disjn(
92    disjn: &Expression,
93    vars_added: &mut HashMap<String, Lit>,
94    inst_in_use: &mut SatInstance,
95) {
96    let cl: &Vec<Expression> = match disjn {
97        Expression::Or(_, vec) => &vec.clone().unwrap_list().unwrap(),
98        _ => panic!(),
99    };
100    let l1 = &cl[0];
101    let l2 = &cl[1];
102
103    // handle literal:
104    let lit1: Lit = handle_lit(l1, vars_added, inst_in_use);
105    // also handle literal
106    let lit2: Lit = handle_lit(l2, vars_added, inst_in_use);
107
108    inst_in_use.add_binary(lit1, lit2);
109}
110
111pub fn handle_cnf(vec_cnf: &Vec<Expression>, vars_added: &mut HashMap<String, Lit>) -> SatInstance {
112    let mut inst = SatInstance::new();
113    for disjn in vec_cnf {
114        handle_disjn(disjn, vars_added, &mut inst);
115    }
116    inst
117}
118
119// Error reserved for future use
120// TODO: Integrate or remove
121#[derive(Error, Debug)]
122pub enum CNFError {
123    #[error("Variable with name `{0}` not found")]
124    VariableNameNotFound(String),
125
126    #[error("Variable with name `{0}` not of right type")]
127    BadVariableType(String),
128
129    #[error("Unexpected Expression `{0}` inside Not(). Only Not(Reference) or Not(Not) allowed!")]
130    UnexpectedExpressionInsideNot(Expression),
131
132    #[error("Unexpected Expression `{0}` as literal. Only Not() or Reference() allowed!")]
133    UnexpectedLiteralExpression(Expression),
134
135    #[error("Unexpected Expression `{0}` inside And(). Only And(vec<Or>) allowed!")]
136    UnexpectedExpressionInsideAnd(Expression),
137
138    #[error("Unexpected Expression `{0}` inside Or(). Only Or(lit, lit) allowed!")]
139    UnexpectedExpressionInsideOr(Expression),
140
141    #[error("Unexpected Expression `{0}` found!")]
142    UnexpectedExpression(Expression),
143}
conjure_core/solver/adaptors/rustsat/convs.rs

conjure_core/solver/adaptors/rustsat/
convs.rs
