/dports/math/cvc4/CVC4-1.7/src/proof/ |
H A D | sat_proof.h | 62 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 D | cnf_proof.h | 44 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 D | sat_proof_implementation.h | 160 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 D | lfsc_proof_printer.h | 48 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 D | lfsc_proof_printer.cpp | 31 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 D | proof_manager.h | 58 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 D | clausal_bitvector_proof.cpp | 55 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 D | clausal_bitvector_proof.h | 58 void registerUsedClause(ClauseId id, prop::SatClause& clause); 64 std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses;
|
H A D | clause_id.h | 29 typedef unsigned ClauseId; typedef
|
H A D | cnf_proof.cpp | 65 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 D | SimpSolver.h | 46 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 D | SimpSolver.h | 52 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 D | Solver.h | 113 …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 D | er_proof.h | 39 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 D | cryptominisat.cpp | 85 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 D | cadical.h | 38 ClauseId addClause(SatClause& clause, bool removable) override; 40 ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override;
|
H A D | cryptominisat.h | 53 ClauseId addClause(SatClause& clause, bool removable) override; 54 ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override;
|
H A D | cadical.cpp | 76 ClauseId CadicalSolver::addClause(SatClause& clause, bool removable) in addClause() 87 ClauseId CadicalSolver::addXorClause(SatClause& clause, in addXorClause()
|
H A D | sat_solver.h | 53 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 D | Solver.h | 179 …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 D | types.hh | 45 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 D | lfsc_proof_printer_black.h | 54 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 D | minisat.h | 44 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 D | SearchBuilder.pm | 979 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 D | bvminisat.h | 73 ClauseId addClause(SatClause& clause, bool removable) override; 75 ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override in addXorClause()
|