Home
last modified time | relevance | path

Searched refs:CVC3 (Results 1 – 25 of 227) sorted by relevance

12345678910

/dports/math/cvc3/cvc3-2.4.1/src/c_interface/
H A Dc_interface.cpp106 return CVC3::Expr((CVC3::ExprValue*)e); in fromExpr()
129 CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; in toOp()
212 CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; in vc_destroyValidityChecker()
269 CVC3::CLFlags& f = *((CVC3::CLFlags*)flags); in vc_setBoolFlag()
279 CVC3::CLFlags& f = *((CVC3::CLFlags*)flags); in vc_setIntFlag()
289 CVC3::CLFlags& f = *((CVC3::CLFlags*)flags); in vc_setStringFlag()
299 CVC3::CLFlags& f = *((CVC3::CLFlags*)flags); in vc_setStrSeqFlag()
322 CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; in vc_realType()
334 CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; in vc_intType()
2476 CVC3::ExprMap<CVC3::Expr> assertions; in vc_getConcreteModel()
[all …]
/dports/math/cvc3/cvc3-2.4.1/src/parser/
H A DPL.y34 namespace CVC3 {
38 #define TMP CVC3::parserTemp
53 ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum in PLerror()
59 namespace CVC3 {
181 CVC3::Expr *node;
421 EXPR = CVC3::Expr();
427 EXPR = CVC3::Expr();
734 $$ = new CVC3::Expr
743 $$ = new CVC3::Expr
1087 $$ = new CVC3::Expr(CVC3::PLprocessUpdates(*$1, *$3));
[all …]
H A Dsmtlib2.y35 namespace CVC3 {
39 #define TMP CVC3::parserTemp
59 ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum in smtlib2error()
74 CVC3::Expr *node;
76 std::pair<std::vector<CVC3::Expr>, std::vector<CVC3::Expr> > *pat_ann;
155 EXPR = CVC3::Expr();
310 $$ = new CVC3::Expr(VC->listExpr("_PUSH", CVC3::Expr(VC->ratExpr((*$2)))));
315 $$ = new CVC3::Expr(VC->listExpr("_POP", CVC3::Expr(VC->ratExpr((*$2)))));
373 $$ = new CVC3::Expr(CVC3::REAL_CONST, *e);
428 CVC3::Expr id = *$1;
[all …]
H A Dsmtlib.y35 namespace CVC3 {
39 #define TMP CVC3::parserTemp
59 ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum in smtliberror()
74 CVC3::Expr *node;
76 std::pair<std::vector<CVC3::Expr>, std::vector<CVC3::Expr> > *pat_ann;
237 CVC3::Expr cmd;
297 CVC3::Expr cmd2;
573 $$ = new std::pair<std::vector<CVC3::Expr>, std::vector<CVC3::Expr> >;
579 $$ = new std::pair<std::vector<CVC3::Expr>, std::vector<CVC3::Expr> >;
1228 e = CVC3::Expr(CVC3::REAL_CONST, e);
[all …]
H A DLisp.y33 namespace CVC3 {
37 #define TMP CVC3::parserTemp
38 #define EXPR CVC3::parserTemp->expr
39 #define VC (CVC3::parserTemp->vc)
40 #define RAT(args) CVC3::newRational args
52 ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum in Lisperror()
54 return CVC3::parserTemp->error(ss.str()); in Lisperror()
64 CVC3::Expr *node;
65 std::vector<CVC3::Expr> *vec;
110 EXPR = CVC3::Expr();
[all …]
H A Dsmtlib2.lex28 namespace CVC3 {
42 if(CVC3::parserTemp->interactive) { in smtlib2input()
44 std::cout << CVC3::parserTemp->getPrompt() << std::flush; in smtlib2input()
46 CVC3::parserTemp->setPrompt2(); in smtlib2input()
71 result = smtlib2input(*CVC3::parserTemp->is, buf, max_size);
135 [\n] { CVC3::parserTemp->lineNum++; }
145 CVC3::parserTemp->lineNum++; }
159 CVC3::parserTemp->lineNum++; }
170 CVC3::parserTemp->lineNum++; }
H A DLisp.lex28 namespace CVC3 {
42 if(CVC3::parserTemp->interactive) { in Lispinput()
44 std::cout << CVC3::parserTemp->getPrompt() << std::flush; in Lispinput()
46 CVC3::parserTemp->setPrompt2(); in Lispinput()
71 result = Lispinput(*CVC3::parserTemp->is, buf, max_size);
H A Dsmtlib.lex28 namespace CVC3 {
42 if(CVC3::parserTemp->interactive) { in smtlibinput()
44 std::cout << CVC3::parserTemp->getPrompt() << std::flush; in smtlibinput()
46 CVC3::parserTemp->setPrompt2(); in smtlibinput()
71 result = smtlibinput(*CVC3::parserTemp->is, buf, max_size);
H A DPL.lex28 namespace CVC3 {
42 if(CVC3::parserTemp->interactive) { in PLinput()
44 std::cout << CVC3::parserTemp->getPrompt() << std::flush; in PLinput()
46 CVC3::parserTemp->setPrompt2(); in PLinput()
71 result = PLinput(*CVC3::parserTemp->is, buf, max_size);
/dports/math/cvc3/cvc3-2.4.1/src/include/
H A Dcnf_manager.h30 namespace CVC3 {
44 CVC3::ValidityChecker* d_vc;
53 CVC3::CNF_Rules* d_rules;
57 CVC3::Expr expr;
69 CVC3::ExprHashMap<CVC3::Theorem> d_iteMap;
122 CVC3::CNF_Rules* createProofRules(CVC3::TheoremManager* tm, const CVC3::CLFlags&);
125 void registerAtom(const CVC3::Expr& e, const CVC3::Theorem& thm);
128 CVC3::Expr concreteExpr(const CVC3::Expr& e, const Lit& literal);
131 CVC3::Theorem concreteThm(const CVC3::Expr& e);
144 CVC3::Theorem replaceITErec(const CVC3::Expr& e, Var v, bool translateOnly);
[all …]
H A Ddpllt_basic.h34 CVC3::ContextManager* d_cm;
46 CVC3::CDO<unsigned> d_pushLevel;
47 CVC3::CDO<bool> d_readyPrev;
48 CVC3::CDO<unsigned> d_prevStackSize;
49 CVC3::CDO<unsigned> d_prevAStackSize;
57 DPLLTBasic(TheoryAPI* theoryAPI, Decider* decider, CVC3::ContextManager* cm,
83 CVC3::QueryResult checkSat(const CNF_Formula& cnf);
84 CVC3::QueryResult continueCheck(const CNF_Formula& cnf);
87 CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*);
H A Ddpllt_minisat.h76 CVC3::QueryResult search();
87 virtual CVC3::QueryResult checkSat(const CNF_Formula& cnf);
88 virtual CVC3::QueryResult continueCheck(const CNF_Formula& cnf);
104 CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*) ;
H A Ddpllt.h154 virtual CVC3::QueryResult checkSat(const CNF_Formula& cnf) = 0;
166 virtual CVC3::QueryResult continueCheck(const CNF_Formula& cnf) = 0;
172 virtual CVC3::Proof getSatProof(CNF_Manager*, CVC3::TheoryCore*) = 0 ;
H A Ddebug.h38 CVC3::fatalError(__FILE__, __LINE__, #cond, msg)
40 namespace CVC3 {
59 #define DBG_PRINT(cond, pre, v, post) if(cond) CVC3::debugger.getOS() \
64 if(cond) CVC3::debugger.getOS() << (msg) << std::endl
69 DBG_PRINT(CVC3::debugger.trace(flag), pre, v, post)
73 DBG_PRINT_MSG(CVC3::debugger.trace(flag), msg)
77 CVC3::debugError(__FILE__, __LINE__, #cond, str)
80 namespace CVC3 {
417 namespace CVC3 {
H A Dcnf.h82 CVC3::Theorem d_reason; //the theorem for the clause, used in proofs. by yeting
106 void setClauseTheorem(CVC3::Theorem thm){ d_reason = thm;} in setClauseTheorem()
108 CVC3::Theorem getClauseTheorem() const { return d_reason;} in getClauseTheorem()
172 CVC3::CDList<Clause> d_formula;
173 CVC3::CDO<unsigned> d_numVars;
177 CD_CNF_Formula(CVC3::Context* context) in CD_CNF_Formula()
/dports/math/cvc3/cvc3-2.4.1/src/sat/
H A Dsat_proof.h39 CVC3::Theorem d_theorem;
43 …CVC3::Proof d_proof; // by yeting, to store the proof. We do not need to set a null value to pr…
45 SatProofNode(CVC3::Theorem theorem) : in SatProofNode()
59 CVC3::Theorem getLeaf() { DebugAssert(isLeaf(), "SatProofNode: getLeaf"); return d_theorem; } in getLeaf()
64 …CVC3::Proof getNodeProof() {DebugAssert(!d_proof.isNull(), "SatProofNode: nodeProof get null"); re… in getNodeProof()
65 void setNodeProof(CVC3::Proof pf) { d_proof=pf;} in setNodeProof()
87 SatProofNode* registerLeaf(CVC3::Theorem theorem) { in registerLeaf()
H A Dminisat_types.cpp37 + sizeof (CVC3::Theorem);
44 Clause* Clause_new(const vector<Lit>& ps, CVC3::Theorem theorem, int id) { in Clause_new()
51 return new (mem) Clause(true, ps, CVC3::Theorem(), id, pushID); in Lemma_new()
57 s_decision = Clause_new(lits, CVC3::Theorem(), -1); in Decision()
66 s_theoryImplication = Clause_new(lits, CVC3::Theorem(), -2); in TheoryImplication()
H A Ddpllt_minisat.cpp30 using namespace CVC3;
258 CVC3::Proof generateSatProof(SAT::SatProofNode* node, CNF_Manager* cnfManager, TheoremProducer* thm… in generateSatProof()
277 const CVC3::Theorem clauseThm = node->getLeaf(); in generateSatProof()
290 CVC3::Proof leftProof = generateSatProof(node->getLeftParent(), cnfManager, thmProducer); in generateSatProof()
291 CVC3::Proof rightProof = generateSatProof(node->getRightParent(), cnfManager, thmProducer); in generateSatProof()
332 CVC3::Theorem theorem = node->getLeaf(); in printSatProof()
378 CVC3::Proof DPLLTMiniSat::getSatProof(CNF_Manager* cnfManager, CVC3::TheoryCore* core){ in getSatProof()
384 CVC3::TheoremProducer* thmProducer = new TheoremProducer(core->getTM()); in getSatProof()
H A Dminisat_types.h107 CVC3::Theorem d_theorem;
119 Clause(bool learnt, const std::vector<Lit>& ps, CVC3::Theorem theorem, in Clause()
130 friend Clause* Clause_new(const std::vector<Lit>& ps, CVC3::Theorem theorem, int id);
153 CVC3::Theorem getTheorem() const { return d_theorem; }; in getTheorem()
182 Clause* Clause_new(const std::vector<Lit>& ps, CVC3::Theorem theorem, int id);
/dports/math/cvc3/cvc3-2.4.1/java/src/cvc3/
H A DJniUtils.cpp10 using namespace CVC3;
51 jstring toJava(JNIEnv* env, CVC3::QueryResult result) { in toJava()
62 jstring toJava(JNIEnv* env, CVC3::FormulaValue result) { in toJava()
72 jstring toJava(JNIEnv* env, CVC3::InputLanguage lang) { in toJava()
99 } else if (dynamic_cast<const CVC3::SoundException*>(&e) != NULL) { in toJava()
101 } else if (dynamic_cast<const CVC3::EvalException*>(&e) != NULL) { in toJava()
103 } else if (dynamic_cast<const CVC3::CLException*>(&e) != NULL) { in toJava()
105 } else if (dynamic_cast<const CVC3::ParserException*>(&e) != NULL) { in toJava()
107 } else if (dynamic_cast<const CVC3::SmtlibException*>(&e) != NULL) { in toJava()
109 } else if (dynamic_cast<const CVC3::DebugException*>(&e) != NULL) { in toJava()
/dports/math/cvc3/cvc3-2.4.1/
H A DINSTALL82 %CVC3 has the following build dependencies:
165 If you compile %CVC3 with native arithmetic, it is possible that %CVC3 may fail
167 an error message and %CVC3 will abort.
176 To build the Java interface to %CVC3, use the
192 following in the top-level %CVC3 directory:
256 <li>cvc3lib: the C++ %CVC3 library</li>
259 <li>cvc3libcli: the .NET %CVC3 library</li>
353 When building %CVC3 on 64-bit platforms, you must compile %CVC3 in the
445 \section installing Installing CVC3
546 Runtime Errors (CVC3 library)
[all …]
/dports/math/cvc4/CVC4-1.7/src/parser/cvc/
H A DREADME9 In order to support our users, we have tried to parse what CVC3 could
12 bug if a particular discrepancy between CVC3 and CVC4 handling of
16 Below is a list of the known differences between CVC3's and CVC4's
19 rapidly expanding, but does not match CVC3's breadth yet. However,
24 SAT/INVALID responses like CVC3 did.
30 This syntax was deprecated in CVC3, and will no longer be
38 list of assertions like CVC3 did.
45 is permissible in CVC4 but not in CVC3.
74 This means that CVC4 may allow you to declare things that CVC3 does
78 a : INT; % CVC3 complains
/dports/math/cvc4/CVC4-1.7/
H A DREADME.md14 CVC3) but does not directly incorporate code from any previous version.
114 CVC3 was a major overhaul of portions of CVC Lite: it added better decision
121 than taking CVC3 and redesigning problem parts, we've taken a clean-room
122 approach, starting from scratch. Before using any designs from CVC3, we have
124 a superficial resemblance, if any, to their correspondent in CVC3.
126 However, CVC4 is fundamentally similar to CVC3 and many other modern SMT
132 performance characteristics of CVC3. CVC3 has many useful features, but some
134 computation (where more nimble engineering approaches could suffice) makes CVC3
135 a much slower prover than other tools. As these designs are central to CVC3, a
/dports/math/cvc3/cvc3-2.4.1/java/include/cvc3/
H A DJniUtils.h155 jstring toJava(JNIEnv* env, CVC3::QueryResult result);
156 jstring toJava(JNIEnv* env, CVC3::FormulaValue result);
157 jstring toJava(JNIEnv* env, CVC3::InputLanguage result);
158 CVC3::InputLanguage toCppInputLanguage(JNIEnv* env, const std::string& lang);
161 void toJava(JNIEnv* env, const CVC3::Exception& e);
266 template <class V> jobjectArray toJavaHCopy(JNIEnv* env, const CVC3::ExprMap<V>& hm) { in toJavaHCopy()
274 typename CVC3::ExprMap<V>::const_iterator it; in toJavaHCopy()
277 env->SetObjectArrayElement(jarray, i, embed_copy<CVC3::Expr>(env, it->first)); in toJavaHCopy()
/dports/math/cvc3/cvc3-2.4.1/doc/
H A Duserdoc.dox3 \page user_doc The CVC3 User's Manual
179 predecessors of CVC3;
199 %%% This is a CVC3 comment
279 But that is just CVC3's way,
524 and are rejected by CVC3:
558 CVC3 provides predefined names
914 can define during a run of CVC3.
1390 CVC3 provides the operator
1400 CVC3 provides the operator
1818 but CVC3 is unable to prove it.
[all …]

12345678910