cvc4_add_example(simple_vc_cxx "" "")
cvc4_add_example(simple_vc_quant_cxx "" "")
-cvc4_add_example(translator "" ""
- # argument to binary (for testing)
- ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2)
+# TODO(project issue $206): Port example to new API
+# cvc4_add_example(translator "" ""
+# # argument to binary (for testing)
+# ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2)
add_subdirectory(api)
-add_subdirectory(hashsmt)
-add_subdirectory(nra-translate)
-add_subdirectory(sets-translate)
+# TODO(project issue $206): Port example to new API
+# add_subdirectory(hashsmt)
+# add_subdirectory(nra-translate)
+# add_subdirectory(sets-translate)
if(TARGET CVC4::cvc4jar)
find_package(Java REQUIRED)
include(UseJava)
- get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE)
-
- add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}")
-
- add_test(
- NAME java/SimpleVC
- COMMAND
- ${Java_JAVA_EXECUTABLE}
- -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar"
- -Djava.library.path=${CVC4_JNI_PATH}
- SimpleVC
- )
+ ## disabled until bindings for the new API are in place (issue #2284)
+ # get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE)
+ #
+ # add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}")
+ #
+ # add_test(
+ # NAME java/SimpleVC
+ # COMMAND
+ # ${Java_JAVA_EXECUTABLE}
+ # -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar"
+ # -Djava.library.path=${CVC4_JNI_PATH}
+ # SimpleVC
+ # )
add_subdirectory(api/java)
endif()
set(EXAMPLES_API_JAVA
- BitVectors
- BitVectorsAndArrays
## disabled until bindings for the new API are in place (issue #2284)
- #CVC4Streams
- Combination
- Datatypes
- Exceptions
- FloatingPointArith
- HelloWorld
- LinearArith
- ## disabled until bindings for the new API are in place (issue #2284)
- #PipedInput
- Relations
- Statistics
- Strings
- UnsatCores
+ # BitVectors
+ # BitVectorsAndArrays
+ # CVC4Streams
+ # Combination
+ # Datatypes
+ # Exceptions
+ # FloatingPointArith
+ # HelloWorld
+ # LinearArith
+ # PipedInput
+ # Relations
+ # Statistics
+ # Strings
+ # UnsatCores
)
foreach(example ${EXAMPLES_API_JAVA})
** identical.
**/
-#include <iostream>
+#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
+#include <iostream>
-using namespace std;
-using namespace CVC4;
+using namespace CVC4::api;
int main() {
- ExprManager em;
- SmtEngine smt(&em);
+ Solver slv;
// Prove that for integers x and y:
// x > 0 AND y > 0 => 2x + y >= 3
- Type integer = em.integerType();
+ Sort integer = slv.getIntegerSort();
- Expr x = em.mkVar("x", integer);
- Expr y = em.mkVar("y", integer);
- Expr zero = em.mkConst(Rational(0));
+ Term x = slv.mkConst(integer, "x");
+ Term y = slv.mkConst(integer, "y");
+ Term zero = slv.mkReal(0);
- Expr x_positive = em.mkExpr(kind::GT, x, zero);
- Expr y_positive = em.mkExpr(kind::GT, y, zero);
+ Term x_positive = slv.mkTerm(Kind::GT, x, zero);
+ Term y_positive = slv.mkTerm(Kind::GT, y, zero);
- Expr two = em.mkConst(Rational(2));
- Expr twox = em.mkExpr(kind::MULT, two, x);
- Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y);
+ Term two = slv.mkReal(2);
+ Term twox = slv.mkTerm(Kind::MULT, two, x);
+ Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y);
- Expr three = em.mkConst(Rational(3));
- Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three);
+ Term three = slv.mkReal(3);
+ Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three);
- Expr formula =
- em.mkExpr(kind::AND, x_positive, y_positive).
- impExpr(twox_plus_y_geq_3);
+ Term formula =
+ slv.mkTerm(Kind::AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3);
- cout << "Checking entailment of formula " << formula << " with CVC4." << endl;
- cout << "CVC4 should report ENTAILED." << endl;
- cout << "Result from CVC4 is: " << smt.checkEntailed(formula) << endl;
+ std::cout << "Checking entailment of formula " << formula << " with CVC4."
+ << std::endl;
+ std::cout << "CVC4 should report ENTAILED." << std::endl;
+ std::cout << "Result from CVC4 is: " << slv.checkEntailed(formula)
+ << std::endl;
return 0;
}
** A simple demonstration of the C++ interface for quantifiers.
**/
-#include <iostream>
+#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
+#include <iostream>
-using namespace std;
-using namespace CVC4;
+using namespace CVC4::api;
int main() {
- ExprManager em;
- SmtEngine smt(&em);
+ Solver slv;
// Prove that the following is unsatisfiable:
// forall x. P( x ) ^ ~P( 5 )
- Type integer = em.integerType();
- Type boolean = em.booleanType();
- Type integerPredicate = em.mkFunctionType(integer, boolean);
-
- Expr p = em.mkVar("P", integerPredicate);
- Expr x = em.mkBoundVar("x", integer);
-
+ Sort integer = slv.getIntegerSort();
+ Sort boolean = slv.getBooleanSort();
+ Sort integerPredicate = slv.mkFunctionSort(integer, boolean);
+
+ Term p = slv.mkConst(integerPredicate, "P");
+ Term x = slv.mkVar(integer, "x");
+
// make forall x. P( x )
- Expr var_list = em.mkExpr(kind::BOUND_VAR_LIST, x);
- Expr px = em.mkExpr(kind::APPLY_UF, p, x);
- Expr quantpospx = em.mkExpr(kind::FORALL, var_list, px);
- cout << "Made expression : " << quantpospx << endl;
-
+ Term var_list = slv.mkTerm(Kind::BOUND_VAR_LIST, x);
+ Term px = slv.mkTerm(Kind::APPLY_UF, p, x);
+ Term quantpospx = slv.mkTerm(Kind::FORALL, var_list, px);
+ std::cout << "Made expression : " << quantpospx << std::endl;
+
//make ~P( 5 )
- Expr five = em.mkConst(Rational(5));
- Expr pfive = em.mkExpr(kind::APPLY_UF, p, five);
- Expr negpfive = em.mkExpr(kind::NOT, pfive);
- cout << "Made expression : " << negpfive << endl;
-
- Expr formula = em.mkExpr(kind::AND, quantpospx, negpfive);
+ Term five = slv.mkReal(5);
+ Term pfive = slv.mkTerm(Kind::APPLY_UF, p, five);
+ Term negpfive = slv.mkTerm(Kind::NOT, pfive);
+ std::cout << "Made expression : " << negpfive << std::endl;
- smt.assertFormula(formula);
+ Term formula = slv.mkTerm(Kind::AND, quantpospx, negpfive);
- cout << "Checking SAT after asserting " << formula << " to CVC4." << endl;
- cout << "CVC4 should report unsat." << endl;
- cout << "Result from CVC4 is: " << smt.checkSat() << endl;
+ slv.assertFormula(formula);
+ std::cout << "Checking SAT after asserting " << formula << " to CVC4."
+ << std::endl;
+ std::cout << "CVC4 should report unsat." << std::endl;
+ std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl;
- SmtEngine smtp(&em);
-
- // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x))))
- Expr pattern = em.mkExpr(kind::INST_PATTERN, px);
- Expr pattern_list = em.mkExpr(kind::INST_PATTERN_LIST, pattern);
- Expr quantpospx_pattern = em.mkExpr(kind::FORALL, var_list, px, pattern_list);
- cout << "Made expression : " << quantpospx_pattern << endl;
+ slv.resetAssertions();
- Expr formula_pattern = em.mkExpr(kind::AND, quantpospx_pattern, negpfive);
+ // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x))))
+ Term pattern = slv.mkTerm(Kind::INST_PATTERN, px);
+ Term pattern_list = slv.mkTerm(Kind::INST_PATTERN_LIST, pattern);
+ Term quantpospx_pattern =
+ slv.mkTerm(Kind::FORALL, var_list, px, pattern_list);
+ std::cout << "Made expression : " << quantpospx_pattern << std::endl;
- smtp.assertFormula(formula_pattern);
+ Term formula_pattern = slv.mkTerm(Kind::AND, quantpospx_pattern, negpfive);
- cout << "Checking SAT after asserting " << formula_pattern << " to CVC4." << endl;
- cout << "CVC4 should report unsat." << endl;
- cout << "Result from CVC4 is: " << smtp.checkSat() << endl;
+ slv.assertFormula(formula_pattern);
+ std::cout << "Checking SAT after asserting " << formula_pattern << " to CVC4."
+ << std::endl;
+ std::cout << "CVC4 should report unsat." << std::endl;
+ std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl;
return 0;
}
namespace CVC4 {
+namespace api {
+class Solver;
+}
+
class Expr;
class SmtEngine;
class NodeManager;
class ResourceManager;
class CVC4_PUBLIC ExprManager {
-private:
+ private:
+ friend api::Solver;
/** The internal node manager */
NodeManager* d_nodeManager;
/** A list of datatypes owned by this expr manager. */
std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes;
- public:
/**
* Creates an expression manager with default options.
*/
*/
explicit ExprManager(const Options& options);
+ public:
/**
* Destroys the expression manager. No will be deallocated at this point, so
* any expression references that used to be managed by this expression
#include "theory/quantifiers/candidate_rewrite_database.h"
+#include "api/cvc4cpp.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
// options as the SmtEngine we belong to, where we ensure that
// produce-models is set.
bool needExport = false;
- ExprManager em(nm->getOptions());
- std::unique_ptr<SmtEngine> rrChecker;
+
+ // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+ // This is only temporarily until we have separate options for each
+ // SmtEngine instance. We should reuse the same ExprManager with
+ // a different SmtEngine (and different options) here, eventually.
+ // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+ api::Solver slv(&nm->getOptions());
+ ExprManager* em = slv.getExprManager();
+ SmtEngine* rrChecker = slv.getSmtEngine();
ExprManagerMapCollection varMap;
initializeChecker(rrChecker, em, varMap, crr, needExport);
Result r = rrChecker->checkSat();
Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE);
if (needExport)
{
- Expr erefv = refv.toExpr().exportTo(&em, varMap);
+ Expr erefv = refv.toExpr().exportTo(em, varMap);
val = Node::fromExpr(rrChecker->getValue(erefv).exportTo(
nm->toExprManager(), varMap));
}
#include "theory/quantifiers/expr_miner.h"
+#include "api/cvc4cpp.h"
#include "options/quantifiers_options.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
}
-void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
- ExprManager& em,
+void ExprMiner::initializeChecker(SmtEngine* checker,
+ ExprManager* em,
ExprManagerMapCollection& varMap,
Node query,
bool& needExport)
return Result(Result::SAT);
}
}
+ // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+ // This is only temporarily until we have separate options for each
+ // SmtEngine instance. We should reuse the same ExprManager with
+ // a different SmtEngine (and different options) here, eventually.
+ // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
NodeManager* nm = NodeManager::currentNM();
bool needExport = false;
- ExprManager em(nm->getOptions());
- std::unique_ptr<SmtEngine> smte;
+ api::Solver slv(&nm->getOptions());
+ ExprManager* em = slv.getExprManager();
+ SmtEngine* smte = slv.getSmtEngine();
ExprManagerMapCollection varMap;
initializeChecker(smte, em, varMap, queryr, needExport);
return smte->checkSat();
* (for instance, model values) must be exported to the current expression
* manager.
*/
- void initializeChecker(std::unique_ptr<SmtEngine>& smte,
- ExprManager& em,
+ void initializeChecker(SmtEngine* smte,
+ ExprManager* em,
ExprManagerMapCollection& varMap,
Node query,
bool& needExport);
#include "theory/quantifiers/query_generator.h"
#include <fstream>
+
+#include "api/cvc4cpp.h"
#include "options/quantifiers_options.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
Trace("sygus-qgen-check") << " query: check " << qy << "..." << std::endl;
NodeManager* nm = NodeManager::currentNM();
// make the satisfiability query
+ //
+ // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+ // This is only temporarily until we have separate options for each
+ // SmtEngine instance. We should reuse the same ExprManager with
+ // a different SmtEngine (and different options) here, eventually.
+ // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
bool needExport = false;
- ExprManager em(nm->getOptions());
- std::unique_ptr<SmtEngine> queryChecker;
+ api::Solver slv(&nm->getOptions());
+ ExprManager* em = slv.getExprManager();
+ SmtEngine* queryChecker = slv.getSmtEngine();
ExprManagerMapCollection varMap;
initializeChecker(queryChecker, em, varMap, qy, needExport);
Result r = queryChecker->checkSat();
{
addSuccess = false;
// try a new core
- std::unique_ptr<SmtEngine> checkSol;
- initializeSubsolver(checkSol);
+ std::unique_ptr<SmtEngine> checkSol(
+ new SmtEngine(NodeManager::currentNM()->toExprManager()));
+ initializeSubsolver(checkSol.get());
Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
std::vector<Node> rasserts = asserts;
rasserts.push_back(d_sc);
{
// In terms of Variant #2, this is the check "if S ^ U is unsat"
Trace("sygus-ccore") << "----- Check side condition" << std::endl;
- std::unique_ptr<SmtEngine> checkSc;
- initializeSubsolver(checkSc);
+ std::unique_ptr<SmtEngine> checkSc(
+ new SmtEngine(NodeManager::currentNM()->toExprManager()));
+ initializeSubsolver(checkSc.get());
std::vector<Node> scasserts;
scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
scasserts.push_back(d_sc);
#include "theory/quantifiers/sygus/sygus_repair_const.h"
+#include "api/cvc4cpp.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
return !d_base_inst.isNull() && d_allow_constant_grammar;
}
-void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker,
- ExprManager& em,
- ExprManagerMapCollection& varMap,
- Node query,
- bool& needExport)
-{
- if (options::sygusRepairConstTimeout.wasSetByUser())
- {
- // To support a separate timeout for the subsolver, we need to create
- // a separate ExprManager with its own options. This requires that
- // the expressions sent to the subsolver can be exported from on
- // ExprManager to another.
- initializeSubsolverWithExport(checker,
- em,
- varMap,
- query.toExpr(),
- true,
- options::sygusRepairConstTimeout());
- // renable options disabled by sygus
- checker->setOption("miniscope-quant", true);
- checker->setOption("miniscope-quant-fv", true);
- checker->setOption("quant-split", true);
- }
- else
- {
- needExport = false;
- initializeSubsolver(checker, query.toExpr());
- }
-}
-
bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
const std::vector<Node>& candidate_values,
std::vector<Node>& repair_cv,
Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
// make the satisfiability query
+ //
+ // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+ // This is only temporarily until we have separate options for each
+ // SmtEngine instance. We should reuse the same ExprManager with
+ // a different SmtEngine (and different options) here, eventually.
+ // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
bool needExport = true;
+ std::unique_ptr<SmtEngine> simpleSmte;
+ std::unique_ptr<api::Solver> slv;
+ ExprManager* em = nullptr;
+ SmtEngine* repcChecker = nullptr;
ExprManagerMapCollection varMap;
- ExprManager em(nm->getOptions());
- std::unique_ptr<SmtEngine> repcChecker;
- initializeChecker(repcChecker, em, varMap, fo_body, needExport);
+
+ if (options::sygusRepairConstTimeout.wasSetByUser())
+ {
+ // To support a separate timeout for the subsolver, we need to create
+ // a separate ExprManager with its own options. This requires that
+ // the expressions sent to the subsolver can be exported from on
+ // ExprManager to another.
+ slv.reset(new api::Solver(&nm->getOptions()));
+ em = slv->getExprManager();
+ repcChecker = slv->getSmtEngine();
+ initializeSubsolverWithExport(repcChecker,
+ em,
+ varMap,
+ fo_body.toExpr(),
+ true,
+ options::sygusRepairConstTimeout());
+ // renable options disabled by sygus
+ repcChecker->setOption("miniscope-quant", true);
+ repcChecker->setOption("miniscope-quant-fv", true);
+ repcChecker->setOption("quant-split", true);
+ }
+ else
+ {
+ needExport = false;
+ em = nm->toExprManager();
+ simpleSmte.reset(new SmtEngine(em));
+ repcChecker = simpleSmte.get();
+ initializeSubsolver(repcChecker, fo_body.toExpr());
+ }
+
Result r = repcChecker->checkSat();
Trace("sygus-repair-const") << "...got : " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
Node fov_m;
if (needExport)
{
- Expr e_fov = fov.toExpr().exportTo(&em, varMap);
+ Expr e_fov = fov.toExpr().exportTo(em, varMap);
fov_m = Node::fromExpr(
repcChecker->getValue(e_fov).exportTo(nm->toExprManager(), varMap));
}
* If n is in the given logic, this method returns true.
*/
bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar);
- /** initialize checker
- *
- * This function initializes the smt engine checker to check the
- * satisfiability of the argument "query"
- *
- * The arguments em and varMap are used for supporting cases where we
- * want checker to use a different expression manager instead of the current
- * expression manager. The motivation for this so that different options can
- * be set for the subcall.
- *
- * We update the flag needExport to true if checker is using the expression
- * manager em. In this case, subsequent expressions extracted from smte
- * (for instance, model values) must be exported to the current expression
- * manager.
- */
- void initializeChecker(std::unique_ptr<SmtEngine>& checker,
- ExprManager& em,
- ExprManagerMapCollection& varMap,
- Node query,
- bool& needExport);
};
} /* CVC4::theory::quantifiers namespace */
if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
{
// create new smt engine to do quantifier elimination
- std::unique_ptr<SmtEngine> smt_qe;
- initializeSubsolver(smt_qe);
+ std::unique_ptr<SmtEngine> smt_qe(
+ new SmtEngine(NodeManager::currentNM()->toExprManager()));
+ initializeSubsolver(smt_qe.get());
Trace("cegqi-qep") << "Property is non-ground single invocation, run "
"QE to obtain single invocation."
<< std::endl;
#include "theory/smt_engine_subsolver.h"
+#include "api/cvc4cpp.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/rewriter.h"
return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
}
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte)
+void initializeSubsolver(SmtEngine* smte)
{
- NodeManager* nm = NodeManager::currentNM();
- smte.reset(new SmtEngine(nm->toExprManager()));
smte->setIsInternalSubsolver();
smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
}
-void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
- ExprManager& em,
+void initializeSubsolverWithExport(SmtEngine* smte,
+ ExprManager* em,
ExprManagerMapCollection& varMap,
Node query,
bool needsTimeout,
// OptionException.
try
{
- smte.reset(new SmtEngine(&em));
smte->setIsInternalSubsolver();
if (needsTimeout)
{
smte->setTimeLimit(timeout, true);
}
smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
- Expr equery = query.toExpr().exportTo(&em, varMap);
+ Expr equery = query.toExpr().exportTo(em, varMap);
smte->assertFormula(equery);
}
catch (const CVC4::ExportUnsupportedException& e)
}
}
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query)
+void initializeSubsolver(SmtEngine* smte, Node query)
{
initializeSubsolver(smte);
smte->assertFormula(query.toExpr());
}
-Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, Node query)
+Result checkWithSubsolver(SmtEngine* smte, Node query)
{
Assert(query.getType().isBoolean());
Result r = quickCheck(query);
}
return r;
}
- std::unique_ptr<SmtEngine> smte;
+
+ // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+ // This is only temporarily until we have separate options for each
+ // SmtEngine instance. We should reuse the same ExprManager with
+ // a different SmtEngine (and different options) here, eventually.
+ // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+ std::unique_ptr<SmtEngine> simpleSmte;
+ std::unique_ptr<api::Solver> slv;
+ ExprManager* em = nullptr;
+ SmtEngine* smte = nullptr;
ExprManagerMapCollection varMap;
NodeManager* nm = NodeManager::currentNM();
- ExprManager em(nm->getOptions());
bool needsExport = false;
if (needsTimeout)
{
+ slv.reset(new api::Solver(&nm->getOptions()));
+ em = slv->getExprManager();
+ smte = slv->getSmtEngine();
needsExport = true;
initializeSubsolverWithExport(
smte, em, varMap, query, needsTimeout, timeout);
}
else
{
+ em = nm->toExprManager();
+ simpleSmte.reset(new SmtEngine(em));
+ smte = simpleSmte.get();
initializeSubsolver(smte, query);
}
r = smte->checkSat();
Expr val;
if (needsExport)
{
- Expr ev = v.toExpr().exportTo(&em, varMap);
+ Expr ev = v.toExpr().exportTo(em, varMap);
val = smte->getValue(ev).exportTo(nm->toExprManager(), varMap);
}
else
* This function initializes the smt engine smte as a subsolver, e.g. it
* creates a new SMT engine and sets the options of the current SMT engine.
*/
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte);
+void initializeSubsolver(SmtEngine* smte);
/**
* Initialize Smt subsolver with exporting
* manager.
*
* @param smte The smt engine pointer to initialize
- * @param em Reference to the expression manager to use
+ * @param em Reference to the expression manager used by smte
* @param varMap Map used for exporting expressions
* @param query The query to check
* @param needsTimeout Whether we would like to set a timeout
* @param timeout The timeout (in milliseconds)
*/
-void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
- ExprManager& em,
+void initializeSubsolverWithExport(SmtEngine* smte,
+ ExprManager* em,
ExprManagerMapCollection& varMap,
Node query,
bool needsTimeout = false,
* exporting since the Options and ExprManager are tied together.
* TODO: eliminate this dependency (cvc4-projects #120).
*/
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query);
+void initializeSubsolver(SmtEngine* smte, Node query);
/**
* This returns the result of checking the satisfiability of formula query.
* If necessary, smte is initialized to the SMT engine that checked its
* satisfiability.
*/
-Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, Node query);
+Result checkWithSubsolver(SmtEngine* smte, Node query);
/**
* This returns the result of checking the satisfiability of formula query.
cvc4_add_system_test(sep_log_api)
cvc4_add_system_test(smt2_compliance)
cvc4_add_system_test(statistics)
-cvc4_add_system_test(two_smt_engines)
+cvc4_add_system_test(two_solvers)
# TODO: Move CVC4JavaTest.java to test/java and delete run_java_test (after full cmake migration)
#include <iostream>
#include <sstream>
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
+#include "api/cvc4cpp.h"
-using namespace CVC4;
+using namespace CVC4::api;
using namespace std;
int main() {
- ExprManager em;
- Options opts;
- SmtEngine smt(&em);
- Result r = smt.checkEntailed(em.mkConst(true));
-
- return (Result::ENTAILED == r) ? 0 : 1;
+ Solver slv;
+ Result r = slv.checkEntailed(slv.mkBoolean(true));
+ return r.isEntailed() ? 0 : 1;
}
#include <iostream>
#include <sstream>
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
+#include "api/cvc4cpp.h"
-using namespace CVC4;
+using namespace CVC4::api;
int main()
{
- ExprManager em;
- SmtEngine smt(&em);
-
- smt.setOption("incremental", SExpr(true));
-
- Type real = em.realType();
- Expr x = em.mkVar("x", real);
- Expr four = em.mkConst(Rational(4));
- Expr xEqFour = em.mkExpr(Kind::EQUAL, x, four);
- smt.assertFormula(xEqFour);
- std::cout << smt.checkSat() << std::endl;
-
- smt.resetAssertions();
-
- Type elementType = em.integerType();
- Type indexType = em.integerType();
- Type arrayType = em.mkArrayType(indexType, elementType);
- Expr array = em.mkVar("array", arrayType);
- Expr arrayAtFour = em.mkExpr(Kind::SELECT, array, four);
- Expr ten = em.mkConst(Rational(10));
- Expr arrayAtFour_eq_ten = em.mkExpr(Kind::EQUAL, arrayAtFour, ten);
- smt.assertFormula(arrayAtFour_eq_ten);
- std::cout << smt.checkSat() << std::endl;
+ Solver slv;
+ slv.setOption("incremental", "true");
+
+ Sort real = slv.getRealSort();
+ Term x = slv.mkConst(real, "x");
+ Term four = slv.mkReal(4);
+ Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four);
+ slv.assertFormula(xEqFour);
+ std::cout << slv.checkSat() << std::endl;
+
+ slv.resetAssertions();
+
+ Sort elementType = slv.getIntegerSort();
+ Sort indexType = slv.getIntegerSort();
+ Sort arrayType = slv.mkArraySort(indexType, elementType);
+ Term array = slv.mkConst(arrayType, "array");
+ Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four);
+ Term ten = slv.mkReal(10);
+ Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten);
+ slv.assertFormula(arrayAtFour_eq_ten);
+ std::cout << slv.checkSat() << std::endl;
}
** minimally functional.
**/
+#include "util/statistics.h"
+
#include <iostream>
#include <sstream>
+#include "api/cvc4cpp.h"
#include "expr/expr.h"
#include "smt/smt_engine.h"
#include "util/sexpr.h"
-#include "util/statistics.h"
using namespace CVC4;
using namespace std;
int main() {
- ExprManager em;
- Options opts;
- SmtEngine smt(&em);
- smt.setOption("incremental", SExpr("true"));
- Expr x = em.mkVar("x", em.integerType());
- Expr y = em.mkVar("y", em.integerType());
- smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5))));
- Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0)));
- Result r = smt.checkEntailed(q);
+ api::Solver slv;
+ ExprManager* em = slv.getExprManager();
+ SmtEngine* smt = slv.getSmtEngine();
+ smt->setOption("incremental", SExpr("true"));
+ Expr x = em->mkVar("x", em->integerType());
+ Expr y = em->mkVar("y", em->integerType());
+ smt->assertFormula(em->mkExpr(
+ kind::GT, em->mkExpr(kind::PLUS, x, y), em->mkConst(Rational(5))));
+ Expr q = em->mkExpr(kind::GT, x, em->mkConst(Rational(0)));
+ Result r = smt->checkEntailed(q);
if (r != Result::NOT_ENTAILED)
{
exit(1);
}
- Statistics stats = smt.getStatistics();
+ Statistics stats = smt->getStatistics();
for(Statistics::iterator i = stats.begin(); i != stats.end(); ++i) {
cout << "stat " << (*i).first << " is " << (*i).second << endl;
}
- smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5))));
- r = smt.checkEntailed(q);
- Statistics stats2 = smt.getStatistics();
+ smt->assertFormula(em->mkExpr(kind::LT, y, em->mkConst(Rational(5))));
+ r = smt->checkEntailed(q);
+ Statistics stats2 = smt->getStatistics();
bool different = false;
for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) {
cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl;
cout << "stat2 " << (*i).first << " is " << (*i).second << endl;
- if(smt.getStatistic((*i).first) != (*i).second) {
- cout << "SMT engine reports different value for statistic "
- << (*i).first << ": " << smt.getStatistic((*i).first) << endl;
+ if (smt->getStatistic((*i).first) != (*i).second)
+ {
+ cout << "SMT engine reports different value for statistic " << (*i).first
+ << ": " << smt->getStatistic((*i).first) << endl;
exit(1);
}
different = different || stats.getStatistic((*i).first) != (*i).second;
+++ /dev/null
-/********************* */
-/*! \file two_smt_engines.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief A simple test of multiple SmtEngines
- **
- ** A simple test of multiple SmtEngines.
- **/
-
-#include <iostream>
-#include <sstream>
-
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
-
-using namespace CVC4;
-using namespace std;
-
-int main() {
- ExprManager em;
- Options opts;
- SmtEngine smt(&em);
- SmtEngine smt2(&em);
- Result r = smt.checkEntailed(em.mkConst(true));
- Result r2 = smt2.checkEntailed(em.mkConst(true));
-
- return r == Result::ENTAILED && r2 == Result::ENTAILED ? 0 : 1;
-}
-
--- /dev/null
+/********************* */
+/*! \file two_smt_engines.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A simple test of multiple SmtEngines
+ **
+ ** A simple test of multiple SmtEngines.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+using namespace std;
+
+int main() {
+ Solver s1;
+ Solver s2;
+ Result r = s1.checkEntailed(s1.mkBoolean(true));
+ Result r2 = s2.checkEntailed(s2.mkBoolean(true));
+ return r.isEntailed() && r2.isEntailed() ? 0 : 1;
+}
+
#include <cxxtest/TestSuite.h>
//Used in some of the tests
-#include <vector>
#include <sstream>
+#include <vector>
+#include "api/cvc4cpp.h"
+#include "expr/attribute.h"
#include "expr/expr_manager.h"
-#include "expr/node_value.h"
+#include "expr/node.h"
#include "expr/node_builder.h"
#include "expr/node_manager.h"
-#include "expr/node.h"
-#include "expr/attribute.h"
+#include "expr/node_value.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
using namespace std;
class AttributeBlack : public CxxTest::TestSuite {
-private:
-
- ExprManager* d_exprManager;
- NodeManager* d_nodeManager;
- SmtEngine* d_smtEngine;
- SmtScope* d_scope;
-
public:
void setUp() override
{
- d_exprManager = new ExprManager();
+ d_slv = new api::Solver();
+ d_exprManager = d_slv->getExprManager();
d_nodeManager = NodeManager::fromExprManager(d_exprManager);
- d_smtEngine = new SmtEngine(d_exprManager);
+ d_smtEngine = d_slv->getSmtEngine();
d_scope = new SmtScope(d_smtEngine);
}
void tearDown() override
{
delete d_scope;
- delete d_smtEngine;
- delete d_exprManager;
+ delete d_slv;
}
struct PrimitiveIntAttributeId {};
delete node;
}
+ private:
+ api::Solver* d_slv;
+ ExprManager* d_exprManager;
+ NodeManager* d_nodeManager;
+ SmtEngine* d_smtEngine;
+ SmtScope* d_scope;
};
#include <sstream>
#include <string>
-#include "expr/expr_manager.h"
-#include "expr/expr.h"
+#include "api/cvc4cpp.h"
#include "base/exception.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
using namespace CVC4;
using namespace CVC4::kind;
using namespace std;
class ExprManagerPublic : public CxxTest::TestSuite {
-private:
-
- ExprManager* d_exprManager;
-
- void checkAssociative(Expr expr, Kind kind, unsigned int numChildren) {
- std::vector<Expr> worklist;
- worklist.push_back(expr);
-
- unsigned int childrenFound = 0;
-
- while( !worklist.empty() ) {
- Expr current = worklist.back();
- worklist.pop_back();
- if( current.getKind() == kind ) {
- for( unsigned int i = 0; i < current.getNumChildren(); ++i ) {
- worklist.push_back( current[i] );
- }
- } else {
- childrenFound++;
- }
- }
-
- TS_ASSERT_EQUALS( childrenFound, numChildren );
- }
-
- std::vector<Expr> mkVars(Type type, unsigned int n) {
- std::vector<Expr> vars;
- for( unsigned int i = 0; i < n; ++i ) {
- vars.push_back( d_exprManager->mkVar(type) );
- }
- return vars;
- }
-
public:
- void setUp() override { d_exprManager = new ExprManager; }
+ void setUp() override
+ {
+ d_slv = new api::Solver();
+ d_exprManager = d_slv->getExprManager();
+ }
void tearDown() override
{
try
{
- delete d_exprManager;
+ delete d_slv;
}
catch (Exception& e)
{
IllegalArgumentException&);
}
+ private:
+ void checkAssociative(Expr expr, Kind kind, unsigned int numChildren)
+ {
+ std::vector<Expr> worklist;
+ worklist.push_back(expr);
+
+ unsigned int childrenFound = 0;
+
+ while (!worklist.empty())
+ {
+ Expr current = worklist.back();
+ worklist.pop_back();
+ if (current.getKind() == kind)
+ {
+ for (unsigned int i = 0; i < current.getNumChildren(); ++i)
+ {
+ worklist.push_back(current[i]);
+ }
+ }
+ else
+ {
+ childrenFound++;
+ }
+ }
+
+ TS_ASSERT_EQUALS(childrenFound, numChildren);
+ }
+
+ std::vector<Expr> mkVars(Type type, unsigned int n)
+ {
+ std::vector<Expr> vars;
+ for (unsigned int i = 0; i < n; ++i)
+ {
+ vars.push_back(d_exprManager->mkVar(type));
+ }
+ return vars;
+ }
+
+ api::Solver* d_slv;
+ ExprManager* d_exprManager;
};
#include <sstream>
#include <string>
+#include "api/cvc4cpp.h"
#include "base/exception.h"
-#include "expr/expr_manager.h"
#include "expr/expr.h"
+#include "expr/expr_manager.h"
#include "options/options.h"
using namespace CVC4;
using namespace std;
class ExprPublic : public CxxTest::TestSuite {
-private:
-
- Options opts;
-
- ExprManager* d_em;
-
- Expr* a_bool;
- Expr* b_bool;
- Expr* c_bool_and;
- Expr* and_op;
- Expr* plus_op;
- Type* fun_type;
- Expr* fun_op;
- Expr* d_apply_fun_bool;
- Expr* null;
-
- Expr* i1;
- Expr* i2;
- Expr* r1;
- Expr* r2;
-
public:
void setUp() override
{
free(argv[0]);
free(argv[1]);
- d_em = new ExprManager(opts);
+ d_slv = new api::Solver(&opts);
+ d_em = d_slv->getExprManager();
a_bool = new Expr(d_em->mkVar("a", d_em->booleanType()));
b_bool = new Expr(d_em->mkVar("b", d_em->booleanType()));
delete b_bool;
delete a_bool;
- delete d_em;
+ delete d_slv;
}
catch (Exception& e)
{
TS_ASSERT(r1->getExprManager() == d_em);
TS_ASSERT(r2->getExprManager() == d_em);
}
+
+ private:
+ Options opts;
+
+ api::Solver* d_slv;
+ ExprManager* d_em;
+
+ Expr* a_bool;
+ Expr* b_bool;
+ Expr* c_bool_and;
+ Expr* and_op;
+ Expr* plus_op;
+ Type* fun_type;
+ Expr* fun_op;
+ Expr* d_apply_fun_bool;
+ Expr* null;
+
+ Expr* i1;
+ Expr* i2;
+ Expr* r1;
+ Expr* r2;
};
#include <sstream>
#include <string>
+#include "api/cvc4cpp.h"
#include "base/check.h"
#include "base/exception.h"
#include "context/context.h"
using namespace std;
class SymbolTableBlack : public CxxTest::TestSuite {
-private:
-
- ExprManager* d_exprManager;
-
public:
void setUp() override
{
try
{
- d_exprManager = new ExprManager;
+ d_slv = new api::Solver();
+ d_exprManager = d_slv->getExprManager();
}
catch (Exception& e)
{
void tearDown() override
{
try {
- delete d_exprManager;
+ delete d_slv;
}
catch (Exception& e)
{
// TODO: What kind of exception gets thrown here?
TS_ASSERT_THROWS(symtab.popScope(), ScopeException&);
}
+
+ private:
+ api::Solver* d_slv;
+ ExprManager* d_exprManager;
};/* class SymbolTableBlack */
#include <cxxtest/TestSuite.h>
#include <iostream>
-#include <string>
#include <sstream>
+#include <string>
+#include "api/cvc4cpp.h"
+#include "expr/expr_manager.h"
#include "expr/kind.h"
#include "expr/type.h"
-#include "expr/expr_manager.h"
#include "util/cardinality.h"
using namespace CVC4;
using namespace std;
class TypeCardinalityPublic : public CxxTest::TestSuite {
- ExprManager* d_em;
-
public:
- void setUp() override { d_em = new ExprManager(); }
+ void setUp() override
+ {
+ d_slv = new api::Solver();
+ d_em = d_slv->getExprManager();
+ }
- void tearDown() override { delete d_em; }
+ void tearDown() override { delete d_slv; }
void testTheBasics()
{
}
}
+ private:
+ api::Solver* d_slv;
+ ExprManager* d_em;
};/* TypeCardinalityPublic */
** Unit tests for symbolic regular expression operations.
**/
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <memory>
+#include <vector>
+
+#include "api/cvc4cpp.h"
#include "expr/node.h"
#include "expr/node_manager.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/strings/regexp_operation.h"
-#include <cxxtest/TestSuite.h>
-#include <iostream>
-#include <memory>
-#include <vector>
-
using namespace CVC4;
using namespace CVC4::kind;
using namespace CVC4::smt;
{
Options opts;
opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
- d_em = new ExprManager(opts);
- d_smt = new SmtEngine(d_em);
+ d_slv = new api::Solver();
+ d_em = d_slv->getExprManager();
+ d_smt = d_slv->getSmtEngine();
d_scope = new SmtScope(d_smt);
d_regExpOpr = new RegExpOpr();
{
delete d_regExpOpr;
delete d_scope;
- delete d_smt;
- delete d_em;
+ delete d_slv;
}
void includes(Node r1, Node r2)
}
private:
+ api::Solver* d_slv;
ExprManager* d_em;
SmtEngine* d_smt;
SmtScope* d_scope;
#include <cxxtest/TestSuite.h>
//Used in some of the tests
-#include <vector>
#include <sstream>
+#include <vector>
+#include "api/cvc4cpp.h"
#include "expr/expr_manager.h"
-#include "expr/node_value.h"
+#include "expr/node.h"
#include "expr/node_builder.h"
#include "expr/node_manager.h"
-#include "expr/node.h"
+#include "expr/node_value.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/rewriter.h"
public:
void setUp() override
{
- d_em = new ExprManager();
- d_smt = new SmtEngine(d_em);
+ d_slv = new api::Solver();
+ d_em = d_slv->getExprManager();
+ d_smt = d_slv->getSmtEngine();
d_scope = new SmtScope(d_smt);
// Ensure that the SMT engine is fully initialized (required for the
// rewriter)
void tearDown() override
{
delete d_scope;
- delete d_smt;
- delete d_em;
+ delete d_slv;
}
void testArrayConst() {
}
private:
+ api::Solver* d_slv;
ExprManager* d_em;
SmtEngine* d_smt;
NodeManager* d_nm;
#include <cxxtest/TestSuite.h>
+#include "api/cvc4cpp.h"
#include "expr/array_store_all.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
using namespace std;
class ArrayStoreAllBlack : public CxxTest::TestSuite {
- ExprManager* d_em;
-
public:
void setUp() override
{
- d_em = new ExprManager();
+ d_slv = new api::Solver();
+ d_em = d_slv->getExprManager();
}
- void tearDown() override
- {
- delete d_em;
- }
+ void tearDown() override { delete d_slv; }
void testStoreAll() {
Type usort = d_em->mkSort("U");
d_em->mkConst(Rational(0)))));
}
+ private:
+ api::Solver* d_slv;
+ ExprManager* d_em;
}; /* class ArrayStoreAllBlack */
**/
#include <cxxtest/TestSuite.h>
+
#include <sstream>
+#include "api/cvc4cpp.h"
#include "expr/datatype.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
using namespace std;
class DatatypeBlack : public CxxTest::TestSuite {
-
- ExprManager* d_em;
- ExprManagerScope* d_scope;
-
public:
void setUp() override
{
- d_em = new ExprManager();
+ d_slv = new api::Solver();
+ d_em = d_slv->getExprManager();
d_scope = new ExprManagerScope(*d_em);
Debug.on("datatypes");
Debug.on("groundterms");
void tearDown() override
{
delete d_scope;
- delete d_em;
+ delete d_slv;
}
void testEnumeration() {
TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntInt)).toType(), pairIntInt);
}
+ private:
+ api::Solver* d_slv;
+ ExprManager* d_em;
+ ExprManagerScope* d_scope;
};/* class DatatypeBlack */
projects / cvc5.git / commitdiff