Home
last modified time | relevance | path

Searched refs:ClauseId (Results 1 – 25 of 53) sorted by relevance

123

/dports/math/cvc4/CVC4-1.7/src/proof/
H A Dsat_proof.h62 ClauseId id;
74 ResChain(ClauseId start);
89 ClauseId d_start;
130 void endResChain(ClauseId id);
163 ClauseId getTrueUnit() const;
164 ClauseId getFalseUnit() const;
199 void refreshProof(ClauseId id);
281 void print(ClauseId id) const;
342 const ClauseId d_nullId;
351 ClauseId d_trueLit;
[all …]
H A Dcnf_proof.h44 typedef std::unordered_set<ClauseId> ClauseIdSet;
83 ClauseId d_trueUnitClause;
85 ClauseId d_falseUnitClause;
89 Node getDefinitionForClause(ClauseId clause);
122 void registerTrueUnitClause(ClauseId clauseId);
123 void registerFalseUnitClause(ClauseId clauseId);
131 void setClauseAssertion(ClauseId clause, Node node);
156 ProofRule getProofRule(ClauseId clause);
157 Node getAssertionForClause(ClauseId clause);
175 virtual void printCnfProofForClause(ClauseId id,
[all …]
H A Dsat_proof_implementation.h160 ResChain<Solver>::ResChain(ClauseId start) in ResChain()
228 ClauseId id = it->first; in ~TSatProof()
481 ClauseId start_id = res.getStart(); in printRes()
491 ClauseId id = steps[i].id; in printRes()
527 ClauseId id = d_clauseId[clause]; in registerClause()
566 ClauseId id = d_unitId[toInt(lit)]; in registerUnitClause()
678 ClauseId reason_id; in removeRedundantFromRes()
732 ClauseId id = getUnitId(start); in startResChain()
784 ClauseId id = resolveUnit(~lit); in resolveOutUnit()
841 ClauseId conflict_id; in finalizeProof()
[all …]
H A Dlfsc_proof_printer.h48 ClauseId id,
89 static void printSatInputProof(const std::vector<ClauseId>& clauses,
110 static void printCMapProof(const std::vector<ClauseId>& clauses,
134 static std::string clauseName(TSatProof<Solver>* satProof, ClauseId id);
146 ClauseId id,
H A Dlfsc_proof_printer.cpp31 ClauseId id) in clauseName()
51 ClauseId id, in printResolution()
67 ClauseId start_id = res.getStart(); in printResolution()
90 ClauseId id, in printAssumptionsResolution()
129 std::set<ClauseId>::iterator it = satProof->getSeenLearnt().begin(); in printResolutions()
149 void LFSCProofPrinter::printSatInputProof(const std::vector<ClauseId>& clauses, in printSatInputProof()
162 void LFSCProofPrinter::printCMapProof(const std::vector<ClauseId>& clauses, in printCMapProof()
191 ClauseId id,
205 ClauseId id,
H A Dproof_manager.h58 const ClauseId ClauseIdEmpty(-1);
59 const ClauseId ClauseIdUndef(-2);
60 const ClauseId ClauseIdError(-3);
99 typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause;
103 typedef std::unordered_set<ClauseId> IdHashSet;
226 static std::string getInputClauseName(ClauseId id, const std::string& prefix = "");
227 static std::string getLemmaClauseName(ClauseId id, const std::string& prefix = "");
228 static std::string getLemmaName(ClauseId id, const std::string& prefix = "");
229 static std::string getLearntClauseName(ClauseId id, const std::string& prefix = "");
H A Dclausal_bitvector_proof.cpp55 int trueClauseId = ClauseId(ProofManager::currentPM()->nextId()); in initCnfProof()
63 int falseClauseId = ClauseId(ProofManager::currentPM()->nextId()); in initCnfProof()
69 void ClausalBitVectorProof::registerUsedClause(ClauseId id, in registerUsedClause()
140 std::vector<ClauseId> usedIds; in printEmptyClauseProof()
169 std::vector<ClauseId> usedIds; in printEmptyClauseProof()
H A Dclausal_bitvector_proof.h58 void registerUsedClause(ClauseId id, prop::SatClause& clause);
64 std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses;
H A Dclause_id.h29 typedef unsigned ClauseId; typedef
H A Dcnf_proof.cpp65 ProofRule CnfProof::getProofRule(ClauseId clause) { in getProofRule()
70 Node CnfProof::getAssertionForClause(ClauseId clause) { in getAssertionForClause()
76 Node CnfProof::getDefinitionForClause(ClauseId clause) { in getDefinitionForClause()
82 void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { in registerConvertedClause()
108 void CnfProof::registerTrueUnitClause(ClauseId clauseId) in registerTrueUnitClause()
120 void CnfProof::registerFalseUnitClause(ClauseId clauseId) in registerFalseUnitClause()
132 void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { in setClauseAssertion()
145 void CnfProof::setClauseDefinition(ClauseId clause, Node definition) { in setClauseDefinition()
445 void LFSCCnfProof::printCnfProofForClause(ClauseId id, in printCnfProofForClause()
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/simp/
H A DSimpSolver.h46 bool addClause (const vec<Lit>& ps, ClauseId& id);
48 bool addClause (Lit p, ClauseId& id); // Add a unit clause to the solver.
49 bool addClause (Lit p, Lit q, ClauseId& id); // Add a binary clause to the solver.
50 bool addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause to the solver.
51 bool addClause_( vec<Lit>& ps, ClauseId& id);
181 inline bool SimpSolver::addClause (const vec<Lit>& ps, ClauseId& id) { ps.copyTo(add_tmp); re… in addClause()
182 inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); ClauseId id; return… in addEmptyClause()
183 inline bool SimpSolver::addClause (Lit p, ClauseId& id) { add_tmp.clear(); add_t… in addClause()
184 inline bool SimpSolver::addClause (Lit p, Lit q, ClauseId& id) { add_tmp.clear(); add_t… in addClause()
185 inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, ClauseId& id) { add_tmp.clear(); add_t… in addClause()
/dports/math/cvc4/CVC4-1.7/src/prop/minisat/simp/
H A DSimpSolver.h52 bool addClause (const vec<Lit>& ps, bool removable, ClauseId& id);
54 bool addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the solver.
55 …bool addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solv…
56 …bool addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to …
57 bool addClause_(vec<Lit>& ps, bool removable, ClauseId& id);
186 inline bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id) in addClause()
188 inline bool SimpSolver::addEmptyClause(bool removable) { add_tmp.clear(); ClauseId id=-1; return… in addEmptyClause()
189 inline bool SimpSolver::addClause (Lit p, bool removable, ClauseId& id) in addClause()
191 inline bool SimpSolver::addClause (Lit p, Lit q, bool removable, ClauseId& id) in addClause()
193 inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id) in addClause()
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/
H A DSolver.h113 …bool addClause (const vec<Lit>& ps, ClauseId& id); // Add a clause to the s…
115 …bool addClause (Lit p, ClauseId& id); // Add a unit clause to …
116 …bool addClause (Lit p, Lit q, ClauseId& id); // Add a binary clause t…
117 …bool addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause …
118 …bool addClause_( vec<Lit>& ps, ClauseId& id); // Add a clause to the s…
434 inline bool Solver::addClause (const vec<Lit>& ps, ClauseId& id) { ps.copyTo(add_tmp);… in addClause()
435 inline bool Solver::addEmptyClause () { add_tmp.clear(); ClauseId tmp; re… in addEmptyClause()
436 inline bool Solver::addClause (Lit p, ClauseId& id) { add_tmp.clear(); ad… in addClause()
437 inline bool Solver::addClause (Lit p, Lit q, ClauseId& id) { add_tmp.clear(); ad… in addClause()
438 inline bool Solver::addClause (Lit p, Lit q, Lit r, ClauseId& id) { add_tmp.clear(); ad… in addClause()
/dports/math/cvc4/CVC4-1.7/src/proof/er/
H A Der_proof.h39 using ClauseUseRecord = std::vector<std::pair<ClauseId, prop::SatClause>>;
147 const std::vector<ClauseId>& getInputClauseIds() const in getInputClauseIds()
197 std::vector<ClauseId> d_inputClauseIds;
/dports/math/cvc4/CVC4-1.7/src/prop/
H A Dcryptominisat.cpp85 ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause, in addXorClause()
109 ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){ in addClause()
123 ClauseId freshId; in addClause()
126 freshId = ClauseId(ProofManager::currentPM()->nextId()); in addClause()
H A Dcadical.h38 ClauseId addClause(SatClause& clause, bool removable) override;
40 ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override;
H A Dcryptominisat.h53 ClauseId addClause(SatClause& clause, bool removable) override;
54 ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override;
H A Dcadical.cpp76 ClauseId CadicalSolver::addClause(SatClause& clause, bool removable) in addClause()
87 ClauseId CadicalSolver::addXorClause(SatClause& clause, in addXorClause()
H A Dsat_solver.h53 virtual ClauseId addClause(SatClause& clause,
60 virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
/dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/
H A DSolver.h179 …bool addClause (const vec<Lit>& ps, bool removable, ClauseId& id); // Add a clause to the solv…
181 …bool addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the…
182 …bool addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to t…
183 …bool addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to …
184 …bool addClause_( vec<Lit>& ps, bool removable, ClauseId& id); // Add a clause to the solv…
513 inline bool Solver::addClause (const vec<Lit>& ps, bool removable, ClauseId& id) in addClause()
515 inline bool Solver::addEmptyClause (bool removable) { add_tmp.clear(); ClauseId tmp; re… in addEmptyClause()
516 inline bool Solver::addClause (Lit p, bool removable, ClauseId& id) in addClause()
518 inline bool Solver::addClause (Lit p, Lit q, bool removable, ClauseId& id) in addClause()
520 inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id) in addClause()
/dports/math/clingo/clingo-5.5.1/libgringo/gringo/output/
H A Dtypes.hh45 using ClauseId = std::pair<Id_t, Id_t>; typedef
47 using Formula = std::vector<ClauseId>;
/dports/math/cvc4/CVC4-1.7/test/unit/proof/
H A Dlfsc_proof_printer_black.h54 std::vector<CVC4::ClauseId> ids{2, 40, 3}; in testPrintSatInputProof()
88 std::vector<CVC4::ClauseId> ids{2, 40, 3}; in testPrintCMapProof()
/dports/math/cvc4/CVC4-1.7/src/prop/minisat/
H A Dminisat.h44 ClauseId addClause(SatClause& clause, bool removable) override;
45 ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override in addXorClause()
/dports/databases/p5-DBIx-SearchBuilder/DBIx-SearchBuilder-1.68/lib/DBIx/
H A DSearchBuilder.pm979 my $ClauseId = $args{'SUBCLAUSE'} || ($args{'ALIAS'} . "." . $args{'FIELD'});
990 $restriction = $self->{'left_joins'}{ $args{'LEFTJOIN'} }{'criteria'}{ $ClauseId } ||= [];
993 $restriction = $self->{'restrictions'}{ $ClauseId } ||= [];
1018 if ( $self->{_open_parens}{ $ClauseId } ) {
1019 @prefix = ('(') x delete $self->{_open_parens}{ $ClauseId };
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/
H A Dbvminisat.h73 ClauseId addClause(SatClause& clause, bool removable) override;
75 ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override in addXorClause()

123