Home
last modified time | relevance | path

Searched refs:literal_vector (Results 1 – 25 of 306) sorted by relevance

12345678910>>...13

/dports/math/py-z3-solver/z3-z3-4.8.10/src/test/
H A Dcnf_backbones.cpp70 sat::literal_vector& lits, in track_clause()
88 sat::literal_vector lits; in track_clauses()
143 …e_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, … in brute_force_consequences()
146 sat::literal_vector asms1(asms); in brute_force_consequences()
161 sat::literal_vector lambda, backbones; in core_chunking()
168 sat::literal_vector gamma, omegaN; in core_chunking()
175 sat::literal_vector asms1(asms); in core_chunking()
184 sat::literal_vector occurs; in core_chunking()
216 sat::literal_vector cons; in core_chunking()
248 vector<sat::literal_vector> conseq; in cnf_backbones()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/test/
H A Dcnf_backbones.cpp70 sat::literal_vector& lits, in track_clause()
88 sat::literal_vector lits; in track_clauses()
143 …e_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, … in brute_force_consequences()
146 sat::literal_vector asms1(asms); in brute_force_consequences()
161 sat::literal_vector lambda, backbones; in core_chunking()
168 sat::literal_vector gamma, omegaN; in core_chunking()
175 sat::literal_vector asms1(asms); in core_chunking()
184 sat::literal_vector occurs; in core_chunking()
216 sat::literal_vector cons; in core_chunking()
248 vector<sat::literal_vector> conseq; in cnf_backbones()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/sat/
H A Dsat_mus.h24 literal_vector m_core;
25 literal_vector m_mus;
44 literal_vector & get_core();
45 void verify_core(literal_vector const& lits);
51 literal_vector& m_lits;
53 scoped_append(literal_vector& lits, literal_vector const& other): in scoped_append()
H A Dsat_aig_finder.h41 literal_vector m_ands;
42 std::function<void (literal head, literal_vector const& ands)> m_on_aig;
48 void validate_and(literal head, literal_vector const& ands, clause const& c);
50 … void validate_clause(literal x, literal y, literal z, vector<literal_vector> const& clauses);
51 void validate_clause(literal_vector const& clause, vector<literal_vector> const& clauses);
55 …void set(std::function<void (literal head, literal_vector const& ands)> const& f) { m_on_aig = f; } in set()
H A Dsat_elim_eqs.h38 void save_elim(literal_vector const & roots, bool_var_vector const & to_elim);
39 void cleanup_clauses(literal_vector const & roots, clause_vector & cs);
40 void cleanup_bin_watches(literal_vector const & roots);
41 bool check_clauses(literal_vector const & roots) const;
42 bool check_clause(clause const& c, literal_vector const& roots) const;
46 void operator()(literal_vector const & roots, bool_var_vector const & to_elim);
H A Dsat_solver.h139 literal_vector m_replay_assign;
174 literal_vector m_trail;
546 literal_vector m_min_core;
633 literal_vector m_lemma;
634 literal_vector m_ext_antecedents;
672 literal_vector m_lemma_min_stack;
696 literal_vector m_user_scope_literals;
698 literal_vector m_aux_literals;
739 lbool find_mutexes(literal_vector const& lits, vector<literal_vector> & mutexes);
741 …lbool get_consequences(literal_vector const& assms, bool_var_vector const& vars, vector<literal_ve…
[all …]
H A Dsat_aig_finder.cpp231 …void aig_finder::validate_clause(literal_vector const& clause, vector<literal_vector> const& claus… in validate_clause()
256 literal_vector clause; in validate_clause()
265 vector<literal_vector> clauses; in validate_and()
266 clauses.push_back(literal_vector(c.size(), c.begin())); in validate_and()
267 literal_vector clause; in validate_and()
281 vector<literal_vector> clauses; in validate_if()
282 clauses.push_back(literal_vector(c0.size(), c0.begin())); in validate_if()
283 if (c1) clauses.push_back(literal_vector(c1->size(), c1->begin())); in validate_if()
284 if (c2) clauses.push_back(literal_vector(c2->size(), c2->begin())); in validate_if()
285 if (c3) clauses.push_back(literal_vector(c3->size(), c3->begin())); in validate_if()
[all …]
H A Dsat_model_converter.h73 … literal_vector m_clauses; // the different clauses are separated by null_literal
74 literal_vector m_clause; // original clause in case of CCE
88 void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const;
94 void swap(bool_var v, unsigned sz, literal_vector& clause);
111 void insert(entry & c, literal_vector const& covered_clause);
115 void add_ate(literal_vector const& lits);
144 void expand(literal_vector& update_stack);
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/
H A Dsat_mus.h24 literal_vector m_core;
25 literal_vector m_mus;
44 literal_vector & get_core();
45 void verify_core(literal_vector const& lits);
51 literal_vector& m_lits;
53 scoped_append(literal_vector& lits, literal_vector const& other):
H A Dsat_aig_finder.h41 literal_vector m_ands;
42 std::function<void (literal head, literal_vector const& ands)> m_on_aig;
48 void validate_and(literal head, literal_vector const& ands, clause const& c);
50 … void validate_clause(literal x, literal y, literal z, vector<literal_vector> const& clauses);
51 void validate_clause(literal_vector const& clause, vector<literal_vector> const& clauses);
56 …void set(std::function<void (literal head, literal_vector const& ands)> const& f) { m_on_aig = f; } in set()
H A Dsat_elim_eqs.h38 void save_elim(literal_vector const & roots, bool_var_vector const & to_elim);
39 void cleanup_clauses(literal_vector const & roots, clause_vector & cs);
40 void cleanup_bin_watches(literal_vector const & roots);
41 bool check_clauses(literal_vector const & roots) const;
42 bool check_clause(clause const& c, literal_vector const& roots) const;
46 void operator()(literal_vector const & roots, bool_var_vector const & to_elim);
H A Dsat_solver.h131 literal_vector m_replay_assign;
166 literal_vector m_trail;
504 literal_vector m_min_core;
591 literal_vector m_lemma;
592 literal_vector m_ext_antecedents;
630 literal_vector m_lemma_min_stack;
654 literal_vector m_user_scope_literals;
656 literal_vector m_aux_literals;
697 lbool find_mutexes(literal_vector const& lits, vector<literal_vector> & mutexes);
699 …lbool get_consequences(literal_vector const& assms, bool_var_vector const& vars, vector<literal_ve…
[all …]
H A Dsat_aig_finder.cpp231 …void aig_finder::validate_clause(literal_vector const& clause, vector<literal_vector> const& claus… in validate_clause()
256 literal_vector clause; in validate_clause()
265 vector<literal_vector> clauses; in validate_and()
266 clauses.push_back(literal_vector(c.size(), c.begin())); in validate_and()
267 literal_vector clause; in validate_and()
281 vector<literal_vector> clauses; in validate_if()
282 clauses.push_back(literal_vector(c0.size(), c0.begin())); in validate_if()
283 if (c1) clauses.push_back(literal_vector(c1->size(), c1->begin())); in validate_if()
284 if (c2) clauses.push_back(literal_vector(c2->size(), c2->begin())); in validate_if()
285 if (c3) clauses.push_back(literal_vector(c3->size(), c3->begin())); in validate_if()
[all …]
H A Dsat_model_converter.h73 … literal_vector m_clauses; // the different clauses are separated by null_literal
74 literal_vector m_clause; // original clause in case of CCE
88 void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const;
94 void swap(bool_var v, unsigned sz, literal_vector& clause);
111 void insert(entry & c, literal_vector const& covered_clause);
115 void add_ate(literal_vector const& lits);
144 void expand(literal_vector& update_stack);
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/
H A Dba_solver.h107 literal_vector m_lemma;
108 literal_vector m_skipped;
111 literal_vector m_parity_trail;
117 typedef sat::literal_vector pliteral_vector;
149 literal_vector m_roots;
156 bool subsumes(card& c1, card& c2, literal_vector& comp);
348 void push_lit(literal_vector& lits, literal lit);
369 bool all_distinct(literal_vector const& lits);
386 void convert_pb_args(app* t, literal_vector& lits);
403 void add_xr(literal_vector const& lits);
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/util/
H A Dsorting_network.h370 literal_vector Xs; in le()
396 literal_vector Xs; in cmp()
518 … literal mk_add_circuit(literal_vector const& x, literal_vector const& y, literal_vector& out) { in mk_add_circuit()
593 literal mk_ge(literal_vector const& x, literal_vector const& y) { in mk_ge()
656 literal_vector xs; in mk_and()
662 literal_vector xs; in mk_and()
698 literal_vector ors; in mk_exactly_1()
733 literal_vector ands; in mk_at_most_1()
795 literal_vector ands; in mk_at_most_1_small()
849 literal_vector ys; in mk_ordered_1()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/util/
H A Dsorting_network.h370 literal_vector Xs; in le()
396 literal_vector Xs; in cmp()
518 … literal mk_add_circuit(literal_vector const& x, literal_vector const& y, literal_vector& out) { in mk_add_circuit()
593 literal mk_ge(literal_vector const& x, literal_vector const& y) { in mk_ge()
656 literal_vector xs; in mk_and()
662 literal_vector xs; in mk_and()
698 literal_vector ors; in mk_exactly_1()
733 literal_vector ands; in mk_at_most_1()
795 literal_vector ands; in mk_at_most_1_small()
849 literal_vector ys; in mk_ordered_1()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/
H A Dpb_solver.h101 literal_vector m_lemma;
102 literal_vector m_skipped;
105 literal_vector m_parity_trail;
111 typedef sat::literal_vector pliteral_vector;
143 literal_vector m_roots;
150 bool subsumes(card& c1, card& c2, literal_vector& comp);
240 bool is_cardinality(pbc const& p, literal_vector& lits);
325 void push_lit(literal_vector& lits, literal lit);
344 bool all_distinct(literal_vector const& lits);
360 void convert_pb_args(app* t, literal_vector& lits);
[all …]
H A Dxor_solver.d69 void ba_solver::add_xr(literal_vector const& lits) { in add_xr()
73 bool ba_solver::all_distinct(literal_vector const& lits) { in all_distinct()
92 literal ba_solver::add_xor_def(literal_vector& lits, bool learned) { in add_xor_def()
142 constraint* ba_solver::add_xr(literal_vector const& _lits, bool learned) { in add_xr()
143 literal_vector lits; in add_xr()
314 literal_vector lits; in pre_simplify()
363 literal_vector lits, dups; in merge_xor()
407 …std::function<void (literal_vector const&)> f = [this](literal_vector const& l) { add_xr(l, false)… in extract_xor()
424 void get_antecedents(literal l, xr const& x, literal_vector & r);
433 constraint* add_xr(literal_vector const& lits, bool learned);
[all …]
/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dsmt_conflict_resolution.h51 literal_vector const & m_assigned_literals;
55 literal_vector m_lemma;
65 literal_vector * m_antecedents;
109 literal_vector m_assumptions;
170 void justification2literals_core(justification * js, literal_vector & result) ;
174 literal_vector m_tmp_literal_vector;
207 literal_vector const & assigned_literals,
251 literal_vector::const_iterator begin_unsat_core() const { in begin_unsat_core()
255 literal_vector::const_iterator end_unsat_core() const { in end_unsat_core()
259 void justification2literals(justification * js, literal_vector & result);
[all …]
H A Dtheory_pb.h192 literal_vector m_args;
277 literal_vector m_literals; // temporary vector
319 void add_clause(card& c, literal_vector const& lits);
336 void add_clause(ineq& c, literal_vector const& lits);
338 literal_vector& get_lits();
340 literal_vector& get_all_literals(ineq& c, bool negate);
341 literal_vector& get_helpful_literals(ineq& c, bool negate);
350 literal_vector m_resolved;
357 literal_vector m_antecedents;
396 bool validate_antecedents(literal_vector const& lits);
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dsmt_conflict_resolution.h51 literal_vector const & m_assigned_literals;
55 literal_vector m_lemma;
65 literal_vector * m_antecedents;
109 literal_vector m_assumptions;
170 void justification2literals_core(justification * js, literal_vector & result) ;
174 literal_vector m_tmp_literal_vector;
207 literal_vector const & assigned_literals,
251 literal_vector::const_iterator begin_unsat_core() const { in begin_unsat_core()
255 literal_vector::const_iterator end_unsat_core() const { in end_unsat_core()
259 void justification2literals(justification * js, literal_vector & result);
[all …]
H A Dtheory_pb.h192 literal_vector m_args;
277 literal_vector m_literals; // temporary vector
319 void add_clause(card& c, literal_vector const& lits);
336 void add_clause(ineq& c, literal_vector const& lits);
338 literal_vector& get_lits();
340 literal_vector& get_all_literals(ineq& c, bool negate);
341 literal_vector& get_helpful_literals(ineq& c, bool negate);
350 literal_vector m_resolved;
357 literal_vector m_antecedents;
396 bool validate_antecedents(literal_vector const& lits);
[all …]
/dports/math/z3/z3-z3-4.8.13/src/shell/
H A Ddimacs_frontend.cpp81 static void display_core(sat::solver const& s, vector<sat::literal_vector> const& tracking_clauses)… in display_core()
83 sat::literal_vector const& c = s.get_core(); in display_core()
85 sat::literal_vector const& cls = tracking_clauses[c[i].var()]; in display_core()
94 sat::literal_vector& lits, in track_clause()
95 sat::literal_vector& assumptions, in track_clause()
96 vector<sat::literal_vector>& tracking_clauses) { in track_clause()
107 sat::literal_vector& assumptions, in track_clauses()
108 vector<sat::literal_vector>& tracking_clauses) { in track_clauses()
112 sat::literal_vector lits; in track_clauses()
249 vector<sat::literal_vector> tracking_clauses; in read_dimacs()
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/shell/
H A Ddimacs_frontend.cpp79 static void display_core(sat::solver const& s, vector<sat::literal_vector> const& tracking_clauses)… in display_core()
81 sat::literal_vector const& c = s.get_core(); in display_core()
83 sat::literal_vector const& cls = tracking_clauses[c[i].var()]; in display_core()
92 sat::literal_vector& lits, in track_clause()
93 sat::literal_vector& assumptions, in track_clause()
94 vector<sat::literal_vector>& tracking_clauses) { in track_clause()
105 sat::literal_vector& assumptions, in track_clauses()
106 vector<sat::literal_vector>& tracking_clauses) { in track_clauses()
110 sat::literal_vector lits; in track_clauses()
247 vector<sat::literal_vector> tracking_clauses; in read_dimacs()
[all …]

12345678910>>...13