diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-21 12:14:18 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-21 12:14:18 -0700 |
commit | a72771b2f04eb5f761c9db59435165d7cdcdf688 (patch) | |
tree | cbc1f017578712a147a52d27c12488a03ba231b7 | |
parent | bf3af55b4509ec2abf8806187d8c1765e2d8330c (diff) | |
parent | 331187d557b2c54b079de6348ff1f597a72f50a2 (diff) |
Merge branch 'master' into rmCDAttrrmCDAttr
35 files changed, 781 insertions, 114 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index b29585f3b..3780b0b5b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -118,7 +118,6 @@ option(ENABLE_PROFILING "Enable support for gprof profiling") # > allows to detect if set by user (default: IGNORE) # > only necessary for options set for ENABLE_BEST cvc5_option(USE_ABC "Use ABC for AIG bit-blasting") -cvc5_option(USE_CADICAL "Use CaDiCaL SAT solver") cvc5_option(USE_CLN "Use CLN instead of GMP") cvc5_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") cvc5_option(USE_GLPK "Use GLPK simplex solver") @@ -417,10 +416,7 @@ if(USE_ABC) add_definitions(-DCVC5_USE_ABC ${ABC_ARCH_FLAGS}) endif() -if(USE_CADICAL) - find_package(CaDiCaL REQUIRED) - add_definitions(-DCVC5_USE_CADICAL) -endif() +find_package(CaDiCaL REQUIRED) if(USE_CLN) set(GPL_LIBS "${GPL_LIBS} cln") @@ -651,7 +647,6 @@ print_config("Java bindings " ${BUILD_BINDINGS_JAVA}) print_config("Python2 " ${USE_PYTHON2}) message("") print_config("ABC " ${USE_ABC}) -print_config("CaDiCaL " ${USE_CADICAL}) print_config("CryptoMiniSat " ${USE_CRYPTOMINISAT}) print_config("GLPK " ${USE_GLPK}) print_config("Kissat " ${USE_KISSAT}) @@ -4,6 +4,7 @@ Changes since CVC4 1.8 ====================== New Features: +* CaDiCaL is now a required dependency. * SymFPU is now a required dependency. * New unsat-core production modes based on the new proof infrastructure (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature diff --git a/configure.sh b/configure.sh index 25203f8a6..4ba153a75 100755 --- a/configure.sh +++ b/configure.sh @@ -59,7 +59,6 @@ The following flags enable optional packages (disable with --no-<option name>). --cln use CLN instead of GMP --glpk use GLPK simplex solver --abc use the ABC AIG library - --cadical use the CaDiCaL SAT solver [default=yes] --cryptominisat use the CryptoMiniSat SAT solver --kissat use the Kissat SAT solver --poly use the LibPoly library [default=yes] @@ -108,7 +107,6 @@ abc=default asan=default assertions=default auto_download=default -cadical=ON cln=default comp_inc=default coverage=default @@ -174,7 +172,6 @@ do # Best configuration --best) abc=ON - cadical=ON cln=ON cryptominisat=ON glpk=ON @@ -198,9 +195,6 @@ do --name) die "missing argument to $1 (try -h)" ;; --name=*) build_dir=${1##*=} ;; - --cadical) cadical=ON;; - --no-cadical) cadical=OFF;; - --cln) cln=ON;; --no-cln) cln=OFF;; @@ -379,8 +373,6 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_EDITLINE=$editline" [ $abc != default ] \ && cmake_opts="$cmake_opts -DUSE_ABC=$abc" -[ $cadical != default ] \ - && cmake_opts="$cmake_opts -DUSE_CADICAL=$cadical" [ $cln != default ] \ && cmake_opts="$cmake_opts -DUSE_CLN=$cln" [ $cryptominisat != default ] \ diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d7da67cbe..b3f27b703 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1185,9 +1185,9 @@ if(USE_ABC) target_link_libraries(cvc5 PRIVATE ${ABC_LIBRARIES}) target_include_directories(cvc5 PRIVATE ${ABC_INCLUDE_DIR}) endif() -if(USE_CADICAL) - target_link_libraries(cvc5 PRIVATE CaDiCaL) -endif() + +target_link_libraries(cvc5 PRIVATE CaDiCaL) + if(USE_CLN) target_link_libraries(cvc5 PRIVATE CLN) endif() diff --git a/src/api/java/cvc5/Grammar.java b/src/api/java/cvc5/Grammar.java new file mode 100644 index 000000000..f8c6b05c5 --- /dev/null +++ b/src/api/java/cvc5/Grammar.java @@ -0,0 +1,87 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * The cvc5 java API. + */ + +package cvc5; + +public class Grammar extends AbstractPointer { + // region construction and destruction + Grammar(Solver solver, long pointer) { + super(solver, pointer); + } + + protected static native void deletePointer(long pointer); + + public long getPointer() { + return pointer; + } + + @Override + public void finalize() { + deletePointer(pointer); + } + + // endregion + + /** + * Add \p rule to the set of rules corresponding to \p ntSymbol. + * @param ntSymbol the non-terminal to which the rule is added + * @param rule the rule to add + */ + public void addRule(Term ntSymbol, Term rule) { + addRule(pointer, ntSymbol.getPointer(), rule.getPointer()); + } + + private native void addRule( + long pointer, long ntSymbolPointer, long rulePointer); + + /** + * Add \p rules to the set of rules corresponding to \p ntSymbol. + * @param ntSymbol the non-terminal to which the rules are added + * @param rules the rules to add + */ + public void addRules(Term ntSymbol, Term[] rules) { + long[] pointers = Utils.getPointers(rules); + addRules(pointer, ntSymbol.getPointer(), pointers); + } + + public native void addRules( + long pointer, long ntSymbolPointer, long[] rulePointers); + + /** + * Allow \p ntSymbol to be an arbitrary constant. + * @param ntSymbol the non-terminal allowed to be any constant + */ + void addAnyConstant(Term ntSymbol) { + addAnyConstant(pointer, ntSymbol.getPointer()); + } + + private native void addAnyConstant(long pointer, long ntSymbolPointer); + + /** + * Allow \p ntSymbol to be any input variable to corresponding + * synth-fun/synth-inv with the same sort as \p ntSymbol. + * @param ntSymbol the non-terminal allowed to be any input constant + */ + void addAnyVariable(Term ntSymbol) { + addAnyVariable(pointer, ntSymbol.getPointer()); + } + + private native void addAnyVariable(long pointer, long ntSymbolPointer); + + /** + * @return a string representation of this grammar. + */ + protected native String toString(long pointer); +} diff --git a/src/api/java/jni/cvc5_Grammar.cpp b/src/api/java/jni/cvc5_Grammar.cpp new file mode 100644 index 000000000..95af2108f --- /dev/null +++ b/src/api/java/jni/cvc5_Grammar.cpp @@ -0,0 +1,120 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * The cvc5 Java API. + */ + +#include "cvc5_Grammar.h" + +#include "api/cpp/cvc5.h" +#include "cvc5JavaApi.h" + +using namespace cvc5::api; + +/* + * Class: cvc5_Grammar + * Method: deletePointer + * Signature: (J)V + */ +JNIEXPORT void JNICALL Java_cvc5_Grammar_deletePointer(JNIEnv*, + jclass, + jlong pointer) +{ + delete reinterpret_cast<Grammar*>(pointer); +} + +/* + * Class: cvc5_Grammar + * Method: addRule + * Signature: (JJJ)V + */ +JNIEXPORT void JNICALL Java_cvc5_Grammar_addRule(JNIEnv* env, + jobject, + jlong pointer, + jlong ntSymbolPointer, + jlong rulePointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Grammar* current = reinterpret_cast<Grammar*>(pointer); + Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer); + Term* rule = reinterpret_cast<Term*>(rulePointer); + current->addRule(*ntSymbol, *rule); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Grammar + * Method: addRules + * Signature: (JJ[J)V + */ +JNIEXPORT void JNICALL Java_cvc5_Grammar_addRules(JNIEnv* env, + jobject, + jlong pointer, + jlong ntSymbolPointer, + jlongArray rulePointers) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Grammar* current = reinterpret_cast<Grammar*>(pointer); + Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer); + std::vector<Term> rules = getObjectsFromPointers<Term>(env, rulePointers); + current->addRules(*ntSymbol, rules); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Grammar + * Method: addAnyConstant + * Signature: (JJ)V + */ +JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyConstant(JNIEnv* env, + jobject, + jlong pointer, + jlong ntSymbolPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Grammar* current = reinterpret_cast<Grammar*>(pointer); + Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer); + current->addAnyConstant(*ntSymbol); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Grammar + * Method: addAnyVariable + * Signature: (JJ)V + */ +JNIEXPORT void JNICALL Java_cvc5_Grammar_addAnyVariable(JNIEnv* env, + jobject, + jlong pointer, + jlong ntSymbolPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Grammar* current = reinterpret_cast<Grammar*>(pointer); + Term* ntSymbol = reinterpret_cast<Term*>(ntSymbolPointer); + current->addAnyVariable(*ntSymbol); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Grammar + * Method: toString + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Grammar_toString(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Grammar* current = reinterpret_cast<Grammar*>(pointer); + return env->NewStringUTF(current->toString().c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 9d980267d..623b2f943 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -153,6 +153,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Solver(Options*) except + Sort getBooleanSort() except + Sort getIntegerSort() except + + Sort getNullSort() except + Sort getRealSort() except + Sort getRegExpSort() except + Sort getRoundingModeSort() except + @@ -178,10 +179,10 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkTerm(Op op, const vector[Term]& children) except + Term mkTuple(const vector[Sort]& sorts, const vector[Term]& terms) except + Op mkOp(Kind kind) except + - Op mkOp(Kind kind, Kind k) except + Op mkOp(Kind kind, const string& arg) except + Op mkOp(Kind kind, uint32_t arg) except + Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) except + + Op mkOp(Kind kind, const vector[uint32_t]& args) except + # Sygus related functions Grammar mkSygusGrammar(const vector[Term]& boundVars, const vector[Term]& ntSymbols) except + Term mkSygusVar(Sort sort, const string& symbol) except + @@ -207,9 +208,11 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkRegexpEmpty() except + Term mkRegexpSigma() except + Term mkEmptySet(Sort s) except + + Term mkEmptyBag(Sort s) except + Term mkSepNil(Sort sort) except + Term mkString(const string& s) except + Term mkString(const wstring& s) except + + Term mkString(const string& s, bint useEscSequences) except + Term mkEmptySequence(Sort sort) except + Term mkUniverseSet(Sort sort) except + Term mkBitVector(uint32_t size) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 874c63c3d..4bb9da3d1 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -470,6 +470,11 @@ cdef class Solver: sort.csort = self.csolver.getIntegerSort() return sort + def getNullSort(self): + cdef Sort sort = Sort(self) + sort.csort = self.csolver.getNullSort() + return sort + def getRealSort(self): cdef Sort sort = Sort(self) sort.csort = self.csolver.getRealSort() @@ -672,8 +677,8 @@ cdef class Solver: result.cterm = self.csolver.mkTuple(csorts, cterms) return result - - def mkOp(self, kind k, arg0=None, arg1 = None): + @expand_list_arg(num_req_args=0) + def mkOp(self, kind k, *args): ''' Supports the following uses: Op mkOp(Kind kind) @@ -683,28 +688,30 @@ cdef class Solver: Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1) ''' cdef Op op = Op(self) + cdef vector[int] v - if arg0 is None: + if len(args) == 0: op.cop = self.csolver.mkOp(k.k) - elif arg1 is None: - if isinstance(arg0, kind): - op.cop = self.csolver.mkOp(k.k, (<kind?> arg0).k) - elif isinstance(arg0, str): + elif len(args) == 1: + if isinstance(args[0], str): op.cop = self.csolver.mkOp(k.k, <const string &> - arg0.encode()) - elif isinstance(arg0, int): - op.cop = self.csolver.mkOp(k.k, <int?> arg0) + args[0].encode()) + elif isinstance(args[0], int): + op.cop = self.csolver.mkOp(k.k, <int?> args[0]) + elif isinstance(args[0], list): + for a in args[0]: + v.push_back((<int?> a)) + op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v) else: raise ValueError("Unsupported signature" - " mkOp: {}".format(" X ".join([str(k), str(arg0)]))) - else: - if isinstance(arg0, int) and isinstance(arg1, int): - op.cop = self.csolver.mkOp(k.k, <int> arg0, - <int> arg1) + " mkOp: {}".format(" X ".join([str(k), str(args[0])]))) + elif len(args) == 2: + if isinstance(args[0], int) and isinstance(args[1], int): + op.cop = self.csolver.mkOp(k.k, <int> args[0], <int> args[1]) else: raise ValueError("Unsupported signature" - " mkOp: {}".format(" X ".join([k, arg0, arg1]))) + " mkOp: {}".format(" X ".join([k, args[0], args[1]]))) return op def mkTrue(self): @@ -778,17 +785,24 @@ cdef class Solver: term.cterm = self.csolver.mkEmptySet(s.csort) return term + def mkEmptyBag(self, Sort s): + cdef Term term = Term(self) + term.cterm = self.csolver.mkEmptyBag(s.csort) + return term def mkSepNil(self, Sort sort): cdef Term term = Term(self) term.cterm = self.csolver.mkSepNil(sort.csort) return term - def mkString(self, str s): + def mkString(self, str s, useEscSequences = None): cdef Term term = Term(self) cdef Py_ssize_t size cdef wchar_t* tmp = PyUnicode_AsWideCharString(s, &size) - term.cterm = self.csolver.mkString(c_wstring(tmp, size)) + if isinstance(useEscSequences, bool): + term.cterm = self.csolver.mkString(s.encode(), <bint> useEscSequences) + else: + term.cterm = self.csolver.mkString(c_wstring(tmp, size)) PyMem_Free(tmp) return term diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 1befb34ea..c6b004574 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -120,24 +120,23 @@ std::string Configuration::copyright() { << "See licenses/antlr3-LICENSE for copyright and licensing information." << "\n\n"; - if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical() + ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n" + << "third party libraries.\n\n"; + + ss << " CaDiCaL - Simplified Satisfiability Solver\n" + << " See https://github.com/arminbiere/cadical for copyright " + << "information.\n\n"; + + if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCryptominisat() || Configuration::isBuiltWithKissat() || Configuration::isBuiltWithEditline()) { - ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n" - << "third party libraries.\n\n"; if (Configuration::isBuiltWithAbc()) { ss << " ABC - A System for Sequential Synthesis and Verification\n" << " See http://bitbucket.org/alanmi/abc for copyright and\n" << " licensing information.\n\n"; } - if (Configuration::isBuiltWithCadical()) - { - ss << " CaDiCaL - Simplified Satisfiability Solver\n" - << " See https://github.com/arminbiere/cadical for copyright " - << "information.\n\n"; - } if (Configuration::isBuiltWithCryptominisat()) { ss << " CryptoMiniSat - An Advanced SAT Solver\n" @@ -241,8 +240,6 @@ bool Configuration::isBuiltWithAbc() { return IS_ABC_BUILD; } -bool Configuration::isBuiltWithCadical() { return IS_CADICAL_BUILD; } - bool Configuration::isBuiltWithCryptominisat() { return IS_CRYPTOMINISAT_BUILD; } diff --git a/src/base/configuration.h b/src/base/configuration.h index 2a7df1b4a..71c79c22e 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -103,8 +103,6 @@ public: static bool isBuiltWithAbc(); - static bool isBuiltWithCadical(); - static bool isBuiltWithCryptominisat(); static bool isBuiltWithKissat(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 39c5e89e9..b348da380 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -96,12 +96,6 @@ namespace cvc5 { # define IS_ABC_BUILD false #endif /* CVC5_USE_ABC */ -#if CVC5_USE_CADICAL -#define IS_CADICAL_BUILD true -#else /* CVC5_USE_CADICAL */ -#define IS_CADICAL_BUILD false -#endif /* CVC5_USE_CADICAL */ - #if CVC5_USE_CRYPTOMINISAT # define IS_CRYPTOMINISAT_BUILD true #else /* CVC5_USE_CRYPTOMINISAT */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index d31d2e58f..07138dce3 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -146,15 +146,6 @@ void OptionsHandler::checkBvSatSolver(const std::string& option, throw OptionException(ss.str()); } - if (m == SatSolverMode::CADICAL && !Configuration::isBuiltWithCadical()) - { - std::stringstream ss; - ss << "option `" << option - << "' requires a CaDiCaL build of cvc5; this binary was not built with " - "CaDiCaL support"; - throw OptionException(ss.str()); - } - if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat()) { std::stringstream ss; @@ -397,7 +388,6 @@ void OptionsHandler::showConfiguration(const std::string& option, print_config_cond("abc", Configuration::isBuiltWithAbc()); print_config_cond("cln", Configuration::isBuiltWithCln()); print_config_cond("glpk", Configuration::isBuiltWithGlpk()); - print_config_cond("cadical", Configuration::isBuiltWithCadical()); print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat()); print_config_cond("gmp", Configuration::isBuiltWithGmp()); print_config_cond("kissat", Configuration::isBuiltWithKissat()); diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 9aee1df22..3b3f80e6c 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -84,11 +84,6 @@ public: const std::string& flag, const std::string& value); - template <class T> - void checkSatSolverEnabled(const std::string& option, - const std::string& flag, - T m); - void checkBvSatSolver(const std::string& option, const std::string& flag, SatSolverMode m); @@ -171,20 +166,6 @@ public: }; /* class OptionHandler */ -template <class T> -void OptionsHandler::checkSatSolverEnabled(const std::string& option, - const std::string& flag, - T m) -{ -#if !defined(CVC5_USE_CRYPTOMINISAT) && !defined(CVC5_USE_CADICAL) \ - && !defined(CVC5_USE_KISSAT) - std::stringstream ss; - ss << "option `" << option - << "' requires cvc5 to be built with CryptoMiniSat or CaDiCaL or Kissat"; - throw OptionException(ss.str()); -#endif -} - } // namespace options } // namespace cvc5 diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index a42b30773..c1cf0338a 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -688,9 +688,9 @@ enum class PfRule : uint32_t //================================================= Array rules // ======== Read over write // Children: (P:(not (= i1 i2))) - // Arguments: ((select (store a i2 e) i1)) + // Arguments: ((select (store a i1 e) i2)) // ---------------------------------------- - // Conclusion: (= (select (store a i2 e) i1) (select a i1)) + // Conclusion: (= (select (store a i1 e) i2) (select a i2)) ARRAYS_READ_OVER_WRITE, // ======== Read over write, contrapositive // Children: (P:(not (= (select (store a i2 e) i1) (select a i1))) diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index ec8919b0b..ddf20f5a1 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -17,8 +17,6 @@ #include "prop/cadical.h" -#ifdef CVC5_USE_CADICAL - #include "base/check.h" #include "util/statistics_registry.h" @@ -191,5 +189,3 @@ CadicalSolver::Statistics::Statistics(StatisticsRegistry& registry, } // namespace prop } // namespace cvc5 - -#endif // CVC5_USE_CADICAL diff --git a/src/prop/cadical.h b/src/prop/cadical.h index b5e26df9f..46c7c7e42 100644 --- a/src/prop/cadical.h +++ b/src/prop/cadical.h @@ -20,8 +20,6 @@ #ifndef CVC5__PROP__CADICAL_H #define CVC5__PROP__CADICAL_H -#ifdef CVC5_USE_CADICAL - #include "prop/sat_solver.h" #include <cadical.hpp> @@ -103,5 +101,4 @@ class CadicalSolver : public SatSolver } // namespace prop } // namespace cvc5 -#endif // CVC5_USE_CADICAL #endif // CVC5__PROP__CADICAL_H diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 40853b33a..4897f8e6a 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -21,14 +21,15 @@ #include "base/output.h" #include "expr/node.h" #include "options/bv_options.h" +#include "printer/printer.h" #include "proof/clause_id.h" #include "prop/minisat/minisat.h" #include "prop/prop_engine.h" #include "prop/theory_proxy.h" #include "smt/dump.h" #include "smt/smt_engine.h" -#include "printer/printer.h" #include "smt/smt_engine_scope.h" +#include "smt/smt_statistics_registry.h" #include "theory/theory.h" #include "theory/theory_engine.h" @@ -52,7 +53,8 @@ CnfStream::CnfStream(SatSolver* satSolver, d_registrar(registrar), d_name(name), d_removable(false), - d_resourceManager(rm) + d_resourceManager(rm), + d_stats(name) { } @@ -139,6 +141,7 @@ void CnfStream::ensureLiteral(TNode n) n.toString().c_str(), n.getType().toString().c_str()); Trace("cnf") << "ensureLiteral(" << n << ")\n"; + TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true); if (hasLiteral(n)) { ensureMappingForLiteral(n); @@ -722,6 +725,7 @@ void CnfStream::convertAndAssert(TNode node, << ", negated = " << (negated ? "true" : "false") << ", removable = " << (removable ? "true" : "false") << ")\n"; d_removable = removable; + TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true); convertAndAssert(node, negated); } @@ -760,5 +764,11 @@ void CnfStream::convertAndAssert(TNode node, bool negated) } } +CnfStream::Statistics::Statistics(const std::string& name) + : d_cnfConversionTime(smtStatisticsRegistry().registerTimer( + name + "::CnfStream::cnfConversionTime")) +{ +} + } // namespace prop } // namespace cvc5 diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 2959ae726..aeed97380 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -309,6 +309,14 @@ class CnfStream { /** Pointer to resource manager for associated SmtEngine */ ResourceManager* d_resourceManager; + + private: + struct Statistics + { + Statistics(const std::string& name); + TimerStat d_cnfConversionTime; + } d_stats; + }; /* class CnfStream */ } // namespace prop diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index fe3a5ecff..62b2f655c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -107,7 +107,8 @@ PropEngine::PropEngine(TheoryEngine* te, userContext, &d_outMgr, rm, - FormulaLitPolicy::TRACK); + FormulaLitPolicy::TRACK, + "prop"); // connect theory proxy d_theoryProxy->finishInit(d_cnfStream); diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 446f72451..0855cbda5 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -53,13 +53,9 @@ SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry& registry, SatSolver* SatSolverFactory::createCadical(StatisticsRegistry& registry, const std::string& name) { -#ifdef CVC5_USE_CADICAL CadicalSolver* res = new CadicalSolver(registry, name); res->init(); return res; -#else - Unreachable() << "cvc5 was not compiled with CaDiCaL support."; -#endif } SatSolver* SatSolverFactory::createKissat(StatisticsRegistry& registry, diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp index 417d345cb..c76a8a2e7 100644 --- a/src/smt/smt_engine_stats.cpp +++ b/src/smt/smt_engine_stats.cpp @@ -25,8 +25,6 @@ SmtEngineStatistics::SmtEngineStatistics(const std::string& name) name + "definitionExpansionTime")), d_numConstantProps( smtStatisticsRegistry().registerInt(name + "numConstantProps")), - d_cnfConversionTime( - smtStatisticsRegistry().registerTimer(name + "cnfConversionTime")), d_numAssertionsPre(smtStatisticsRegistry().registerInt( name + "numAssertionsPreITERemoval")), d_numAssertionsPost(smtStatisticsRegistry().registerInt( diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h index 441721a54..db914b560 100644 --- a/src/smt/smt_engine_stats.h +++ b/src/smt/smt_engine_stats.h @@ -30,8 +30,6 @@ struct SmtEngineStatistics TimerStat d_definitionExpansionTime; /** number of constant propagations found during nonclausal simp */ IntStat d_numConstantProps; - /** time spent converting to CNF */ - TimerStat d_cnfConversionTime; /** Number of assertions before ite removal */ IntStat d_numAssertionsPre; /** Number of assertions after ite removal */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index d7b70f501..f5783ab6b 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -239,7 +239,6 @@ void SmtSolver::processAssertions(Assertions& as) // Push the formula to SAT { Chat() << "converting to CNF..." << endl; - TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime); const std::vector<Node>& assertions = ap.ref(); // It is important to distinguish the input assertions from the skolem // definitions, as the decision justification heuristic treates the latter diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp index a38dfdfe5..357a54b1a 100644 --- a/src/theory/bv/bitblast/simple_bitblaster.cpp +++ b/src/theory/bv/bitblast/simple_bitblaster.cpp @@ -17,6 +17,7 @@ #include "theory/theory_model.h" #include "theory/theory_state.h" +#include "options/bv_options.h" namespace cvc5 { namespace theory { @@ -129,6 +130,15 @@ Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel) return utils::mkConst(bits.size(), value); } +void BBSimple::computeRelevantTerms(std::set<Node>& termSet) +{ + Assert(options::bitblastMode() == options::BitblastMode::EAGER); + for (const auto& var : d_variables) + { + termSet.insert(var); + } +} + bool BBSimple::collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms) { diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h index ebbb2891f..ec0899145 100644 --- a/src/theory/bv/bitblast/simple_bitblaster.h +++ b/src/theory/bv/bitblast/simple_bitblaster.h @@ -53,6 +53,8 @@ class BBSimple : public TBitblaster<Node> /** Create 'bits' for variable 'var'. */ void makeVariable(TNode var, Bits& bits) override; + /** Add d_variables to termSet. */ + void computeRelevantTerms(std::set<Node>& termSet); /** Collect model values for all relevant terms given in 'relevantTerms'. */ bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms); diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index 8ff4318c0..6ccc6c7c1 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -32,7 +32,7 @@ class BVSolver BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr) : d_state(state), d_im(inferMgr){}; - virtual ~BVSolver(){}; + virtual ~BVSolver() {} /** * Returns true if we need an equality engine. If so, we initialize the @@ -71,7 +71,7 @@ class BVSolver virtual bool needsCheckLastEffort() { return false; } - virtual void propagate(Theory::Effort e){}; + virtual void propagate(Theory::Effort e) {} virtual TrustNode explain(TNode n) { @@ -80,17 +80,20 @@ class BVSolver return TrustNode::null(); } + /** Additionally collect terms relevant for collecting model values. */ + virtual void computeRelevantTerms(std::set<Node>& termSet) {} + /** Collect model values in m based on the relevant terms given by termSet */ virtual bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet) = 0; virtual std::string identify() const = 0; - virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }; + virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); } - virtual void ppStaticLearn(TNode in, NodeBuilder& learned){}; + virtual void ppStaticLearn(TNode in, NodeBuilder& learned) {} - virtual void presolve(){}; + virtual void presolve() {} virtual void notifySharedTerm(TNode t) {} diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index dc2c7e2a3..3ae4a7f0a 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -96,17 +96,19 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s, { case options::SatSolverMode::CRYPTOMINISAT: d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat( - smtStatisticsRegistry(), "theory::bv::BVSolverBitblast")); + smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); break; default: d_satSolver.reset(prop::SatSolverFactory::createCadical( - smtStatisticsRegistry(), "theory::bv::BVSolverBitblast")); + smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::")); } d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(), d_bbRegistrar.get(), d_nullContext.get(), nullptr, - smt::currentResourceManager())); + smt::currentResourceManager(), + prop::FormulaLitPolicy::INTERNAL, + "theory::bv::BVSolverBitblast")); } void BVSolverBitblast::postCheck(Theory::Effort level) @@ -236,6 +238,21 @@ TrustNode BVSolverBitblast::explain(TNode n) return d_im.explainLit(n); } +void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet) +{ + /* BITVECTOR_EAGER_ATOM wraps input assertions that may also contain + * equalities. As a result, these equalities are not handled by the equality + * engine and terms below these equalities do not appear in `termSet`. + * We need to make sure that we compute model values for all relevant terms + * in BitblastMode::EAGER and therefore add all variables from the + * bit-blaster to `termSet`. + */ + if (options::bitblastMode() == options::BitblastMode::EAGER) + { + d_bitblaster->computeRelevantTerms(termSet); + } +} + bool BVSolverBitblast::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) { diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 31d9443c8..c5134c6fc 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -64,6 +64,8 @@ class BVSolverBitblast : public BVSolver EqualityStatus getEqualityStatus(TNode a, TNode b) override; + void computeRelevantTerms(std::set<Node>& termSet) override; + bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet) override; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 22b05b026..3d7f11f6d 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -175,6 +175,11 @@ bool TheoryBV::needsCheckLastEffort() return d_internal->needsCheckLastEffort(); } +void TheoryBV::computeRelevantTerms(std::set<Node>& termSet) +{ + return d_internal->computeRelevantTerms(termSet); +} + bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) { return d_internal->collectModelValues(m, termSet); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 4b3a1f3b2..e884f621c 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -83,6 +83,8 @@ class TheoryBV : public Theory TrustNode explain(TNode n) override; + void computeRelevantTerms(std::set<Node>& termSet) override; + /** Collect model values in m based on the relevant terms given by termSet */ bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet) override; diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index 1255bf270..8b3ce944e 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -43,6 +43,10 @@ def test_get_integer_sort(solver): solver.getIntegerSort() +def test_get_null_sort(solver): + solver.getNullSort() + + def test_get_real_sort(solver): solver.getRealSort() @@ -244,6 +248,15 @@ def test_mk_set_sort(solver): slv.mkSetSort(solver.mkBitVectorSort(4)) +def test_mk_bag_sort(solver): + solver.mkBagSort(solver.getBooleanSort()) + solver.mkBagSort(solver.getIntegerSort()) + solver.mkBagSort(solver.mkBitVectorSort(4)) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkBagSort(solver.mkBitVectorSort(4)) + + def test_mk_sequence_sort(solver): solver.mkSequenceSort(solver.getBooleanSort()) solver.mkSequenceSort(\ @@ -277,6 +290,42 @@ def test_mk_tuple_sort(solver): slv.mkTupleSort([solver.getIntegerSort()]) +def test_mk_bit_vector(solver): + size0 = 0 + size1 = 8 + size2 = 32 + val1 = 2 + val2 = 2 + solver.mkBitVector(size1, val1) + solver.mkBitVector(size2, val2) + solver.mkBitVector("1010", 2) + solver.mkBitVector("1010", 10) + solver.mkBitVector("1234", 10) + solver.mkBitVector("1010", 16) + solver.mkBitVector("a09f", 16) + solver.mkBitVector(8, "-127", 10) + with pytest.raises(RuntimeError): + solver.mkBitVector(size0, val1) + with pytest.raises(RuntimeError): + solver.mkBitVector(size0, val2) + with pytest.raises(RuntimeError): + solver.mkBitVector("", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector("10", 3) + with pytest.raises(RuntimeError): + solver.mkBitVector("20", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "101010101", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "-256", 10) + assert solver.mkBitVector("1010", 2) == solver.mkBitVector("10", 10) + assert solver.mkBitVector("1010", 2) == solver.mkBitVector("a", 16) + assert str(solver.mkBitVector(8, "01010101", 2)) == "#b01010101" + assert str(solver.mkBitVector(8, "F", 16)) == "#b00001111" + assert solver.mkBitVector(8, "-1", 10) ==\ + solver.mkBitVector(8, "FF", 16) + + def test_mk_var(solver): boolSort = solver.getBooleanSort() intSort = solver.getIntegerSort() @@ -312,6 +361,26 @@ def test_mk_uninterpreted_const(solver): slv.mkUninterpretedConst(solver.getBooleanSort(), 1) +def test_mk_abstract_value(solver): + solver.mkAbstractValue("1") + with pytest.raises(ValueError): + solver.mkAbstractValue("0") + with pytest.raises(ValueError): + solver.mkAbstractValue("-1") + with pytest.raises(ValueError): + solver.mkAbstractValue("1.2") + with pytest.raises(ValueError): + solver.mkAbstractValue("1/2") + with pytest.raises(ValueError): + solver.mkAbstractValue("asdf") + + solver.mkAbstractValue(1) + with pytest.raises(ValueError): + solver.mkAbstractValue(-1) + with pytest.raises(ValueError): + solver.mkAbstractValue(0) + + def test_mk_floating_point(solver): t1 = solver.mkBitVector(8) t2 = solver.mkBitVector(4) @@ -345,6 +414,17 @@ def test_mk_empty_set(solver): slv.mkEmptySet(s) +def test_mk_empty_bag(solver): + slv = pycvc5.Solver() + s = solver.mkBagSort(solver.getBooleanSort()) + solver.mkEmptyBag(pycvc5.Sort(solver)) + solver.mkEmptyBag(s) + with pytest.raises(RuntimeError): + solver.mkEmptyBag(solver.getBooleanSort()) + with pytest.raises(RuntimeError): + slv.mkEmptyBag(s) + + def test_mk_empty_sequence(solver): slv = pycvc5.Solver() s = solver.mkSequenceSort(solver.getBooleanSort()) @@ -379,6 +459,33 @@ def test_mk_pos_zero(solver): solver.mkPosZero(3, 5) +def test_mk_op(solver): + # mkOp(Kind kind, Kind k) + with pytest.raises(ValueError): + solver.mkOp(kinds.BVExtract, kinds.Equal) + + # mkOp(Kind kind, const std::string& arg) + solver.mkOp(kinds.Divisible, "2147483648") + with pytest.raises(RuntimeError): + solver.mkOp(kinds.BVExtract, "asdf") + + # mkOp(Kind kind, uint32_t arg) + solver.mkOp(kinds.Divisible, 1) + solver.mkOp(kinds.BVRotateLeft, 1) + solver.mkOp(kinds.BVRotateRight, 1) + with pytest.raises(RuntimeError): + solver.mkOp(kinds.BVExtract, 1) + + # mkOp(Kind kind, uint32_t arg1, uint32_t arg2) + solver.mkOp(kinds.BVExtract, 1, 1) + with pytest.raises(RuntimeError): + solver.mkOp(kinds.Divisible, 1, 2) + + # mkOp(Kind kind, std::vector<uint32_t> args) + args = [1, 2, 2] + solver.mkOp(kinds.TupleProject, args) + + def test_mk_pi(solver): solver.mkPi() @@ -526,11 +633,210 @@ def test_mk_sep_nil(solver): slv.mkSepNil(solver.getIntegerSort()) +def test_mk_string(solver): + solver.mkString("") + solver.mkString("asdfasdf") + str(solver.mkString("asdf\\nasdf")) == "\"asdf\\u{5c}nasdf\"" + str(solver.mkString("asdf\\u{005c}nasdf", True)) ==\ + "\"asdf\\u{5c}nasdf\"" + + +def test_mk_term(solver): + bv32 = solver.mkBitVectorSort(32) + a = solver.mkConst(bv32, "a") + b = solver.mkConst(bv32, "b") + v1 = [a, b] + v2 = [a, pycvc5.Term(solver)] + v3 = [a, solver.mkTrue()] + v4 = [solver.mkInteger(1), solver.mkInteger(2)] + v5 = [solver.mkInteger(1), pycvc5.Term(solver)] + v6 = [] + slv = pycvc5.Solver() + + # mkTerm(Kind kind) const + solver.mkPi() + solver.mkTerm(kinds.RegexpEmpty) + solver.mkTerm(kinds.RegexpSigma) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ConstBV) + + # mkTerm(Kind kind, Term child) const + solver.mkTerm(kinds.Not, solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Not, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Not, a) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Not, solver.mkTrue()) + + # mkTerm(Kind kind, Term child1, Term child2) const + solver.mkTerm(kinds.Equal, a, b) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, pycvc5.Term(solver), b) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, a, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, a, solver.mkTrue()) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Equal, a, b) + + # mkTerm(Kind kind, Term child1, Term child2, Term child3) const + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, pycvc5.Term(solver), solver.mkTrue(), + solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), pycvc5.Term(solver), + solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), b) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + solver.mkTrue()) + + # mkTerm(Kind kind, const std::vector<Term>& children) const + solver.mkTerm(kinds.Equal, v1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, v2) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, v3) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Distinct, v6) + + +def test_mk_term_from_op(solver): + bv32 = solver.mkBitVectorSort(32) + a = solver.mkConst(bv32, "a") + b = solver.mkConst(bv32, "b") + v1 = [solver.mkInteger(1), solver.mkInteger(2)] + v2 = [solver.mkInteger(1), pycvc5.Term(solver)] + v3 = [] + v4 = [solver.mkInteger(5)] + slv = pycvc5.Solver() + + # simple operator terms + opterm1 = solver.mkOp(kinds.BVExtract, 2, 1) + opterm2 = solver.mkOp(kinds.Divisible, 1) + + # list datatype + sort = solver.mkParamSort("T") + listDecl = solver.mkDatatypeDecl("paramlist", sort) + cons = solver.mkDatatypeConstructorDecl("cons") + nil = solver.mkDatatypeConstructorDecl("nil") + cons.addSelector("head", sort) + cons.addSelectorSelf("tail") + listDecl.addConstructor(cons) + listDecl.addConstructor(nil) + listSort = solver.mkDatatypeSort(listDecl) + intListSort =\ + listSort.instantiate([solver.getIntegerSort()]) + c = solver.mkConst(intListSort, "c") + lis = listSort.getDatatype() + + # list datatype constructor and selector operator terms + consTerm1 = lis.getConstructorTerm("cons") + consTerm2 = lis.getConstructor("cons").getConstructorTerm() + nilTerm1 = lis.getConstructorTerm("nil") + nilTerm2 = lis.getConstructor("nil").getConstructorTerm() + headTerm1 = lis["cons"].getSelectorTerm("head") + headTerm2 = lis["cons"].getSelector("head").getSelectorTerm() + tailTerm1 = lis["cons"].getSelectorTerm("tail") + tailTerm2 = lis["cons"]["tail"].getSelectorTerm() + + # mkTerm(Op op, Term term) const + solver.mkTerm(kinds.ApplyConstructor, nilTerm1) + solver.mkTerm(kinds.ApplyConstructor, nilTerm2) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, nilTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, consTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplyConstructor, consTerm2) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, headTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.ApplyConstructor, nilTerm1) + + # mkTerm(Op op, Term child) const + solver.mkTerm(opterm1, a) + solver.mkTerm(opterm2, solver.mkInteger(1)) + solver.mkTerm(kinds.ApplySelector, headTerm1, c) + solver.mkTerm(kinds.ApplySelector, tailTerm2, c) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, a) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0)) + with pytest.raises(RuntimeError): + slv.mkTerm(opterm1, a) + + # mkTerm(Op op, Term child1, Term child2) const + solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0), + solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, a, b) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, pycvc5.Term(solver), solver.mkInteger(1)) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.ApplyConstructor,\ + consTerm1,\ + solver.mkInteger(0),\ + solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + + # mkTerm(Op op, Term child1, Term child2, Term child3) const + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, a, b, a) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(1), + pycvc5.Term(solver)) + + # mkTerm(Op op, const std::vector<Term>& children) const + solver.mkTerm(opterm2, v4) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v1) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v2) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v3) + with pytest.raises(RuntimeError): + slv.mkTerm(opterm2, v4) + + def test_mk_true(solver): solver.mkTrue() solver.mkTrue() +def test_mk_tuple(solver): + solver.mkTuple([solver.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)]) + solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")]) + + with pytest.raises(RuntimeError): + solver.mkTuple([], [solver.mkBitVector("101", 2)]) + with pytest.raises(RuntimeError): + solver.mkTuple([solver.mkBitVectorSort(4)], + [solver.mkBitVector("101", 2)]) + with pytest.raises(RuntimeError): + solver.mkTuple([solver.getIntegerSort()], [solver.mkReal("5.3")]) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkTuple([solver.mkBitVectorSort(3)], [slv.mkBitVector("101", 2)]) + with pytest.raises(RuntimeError): + slv.mkTuple([slv.mkBitVectorSort(3)], [solver.mkBitVector("101", 2)]) + + def test_mk_universe_set(solver): solver.mkUniverseSet(solver.getBooleanSort()) with pytest.raises(RuntimeError): diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9ad4f7e8a..444e4c7f6 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -670,6 +670,7 @@ set(regress_0_tests regress0/issue5743.smt2 regress0/issue5947.smt2 regress0/issue6605-2-abd-triv.smt2 + regress0/issue6741.smt2 regress0/ite_arith.smt2 regress0/ite_real_int_type.smtv1.smt2 regress0/ite_real_valid.smtv1.smt2 diff --git a/test/regress/regress0/bv/eager-inc-cadical.smt2 b/test/regress/regress0/bv/eager-inc-cadical.smt2 index 01840dffa..34007f6aa 100644 --- a/test/regress/regress0/bv/eager-inc-cadical.smt2 +++ b/test/regress/regress0/bv/eager-inc-cadical.smt2 @@ -1,4 +1,3 @@ -; REQUIRES: cadical ; COMMAND-LINE: --incremental --bv-sat-solver=cadical --bitblast=eager (set-logic QF_BV) (set-option :incremental true) diff --git a/test/regress/regress0/issue6741.smt2 b/test/regress/regress0/issue6741.smt2 new file mode 100644 index 000000000..0fbf4edeb --- /dev/null +++ b/test/regress/regress0/issue6741.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --bv-solver=bitblast --bitblast=eager --check-models +(set-logic QF_BV) +(set-info :status sat) +(declare-fun x () (_ BitVec 1)) +(declare-fun y () (_ BitVec 1)) +(assert (= y (ite (= x (_ bv1 1)) (_ bv1 1) (_ bv0 1)))) +(assert (= y (_ bv1 1))) +(check-sat) diff --git a/test/unit/api/java/cvc5/GrammarTest.java b/test/unit/api/java/cvc5/GrammarTest.java new file mode 100644 index 000000000..76a80f55e --- /dev/null +++ b/test/unit/api/java/cvc5/GrammarTest.java @@ -0,0 +1,137 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Abdalrhman Mohamed, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Black box testing of the guards of the Java API functions. + */ + +package cvc5; + +import static cvc5.Kind.*; +import static org.junit.jupiter.api.Assertions.*; + +import java.util.Arrays; +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +class GrammarTest { + private Solver d_solver; + + @BeforeEach + void setUp() { + d_solver = new Solver(); + } + + @Test + void addRule() { + Sort bool = d_solver.getBooleanSort(); + Sort integer = d_solver.getIntegerSort(); + + Term nullTerm = d_solver.getNullTerm(); + Term start = d_solver.mkVar(bool); + Term nts = d_solver.mkVar(bool); + + Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + + assertDoesNotThrow(() -> g.addRule(start, d_solver.mkBoolean(false))); + + assertThrows(CVC5ApiException.class, + () -> g.addRule(nullTerm, d_solver.mkBoolean(false))); + assertThrows(CVC5ApiException.class, () -> g.addRule(start, nullTerm)); + assertThrows(CVC5ApiException.class, + () -> g.addRule(nts, d_solver.mkBoolean(false))); + assertThrows( + CVC5ApiException.class, () -> g.addRule(start, d_solver.mkInteger(0))); + assertThrows(CVC5ApiException.class, () -> g.addRule(start, nts)); + + d_solver.synthFun("f", new Term[] {}, bool, g); + + assertThrows(CVC5ApiException.class, + () -> g.addRule(start, d_solver.mkBoolean(false))); + } + + @Test + void addRules() { + Sort bool = d_solver.getBooleanSort(); + Sort integer = d_solver.getIntegerSort(); + + Term nullTerm = d_solver.getNullTerm(); + Term start = d_solver.mkVar(bool); + Term nts = d_solver.mkVar(bool); + + Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + + assertDoesNotThrow( + () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)})); + + assertThrows(CVC5ApiException.class, + () -> g.addRules(nullTerm, new Term[] {d_solver.mkBoolean(false)})); + assertThrows( + CVC5ApiException.class, () -> g.addRules(start, new Term[] {nullTerm})); + assertThrows(CVC5ApiException.class, + () -> g.addRules(nts, new Term[] {d_solver.mkBoolean(false)})); + assertThrows(CVC5ApiException.class, + () -> g.addRules(start, new Term[] {d_solver.mkInteger(0)})); + assertThrows( + CVC5ApiException.class, () -> g.addRules(start, new Term[] {nts})); + + d_solver.synthFun("f", new Term[] {}, bool, g); + + assertThrows(CVC5ApiException.class, + () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)})); + } + + @Test + void addAnyConstant() { + Sort bool = d_solver.getBooleanSort(); + + Term nullTerm = d_solver.getNullTerm(); + Term start = d_solver.mkVar(bool); + Term nts = d_solver.mkVar(bool); + + Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + + assertDoesNotThrow(() -> g.addAnyConstant(start)); + assertDoesNotThrow(() -> g.addAnyConstant(start)); + + assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(nullTerm)); + assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(nts)); + + d_solver.synthFun("f", new Term[] {}, bool, g); + + assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(start)); + } + + @Test + void addAnyVariable() { + Sort bool = d_solver.getBooleanSort(); + + Term nullTerm = d_solver.getNullTerm(); + Term x = d_solver.mkVar(bool); + Term start = d_solver.mkVar(bool); + Term nts = d_solver.mkVar(bool); + + Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start}); + Grammar g2 = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start}); + + assertDoesNotThrow(() -> g1.addAnyVariable(start)); + assertDoesNotThrow(() -> g1.addAnyVariable(start)); + assertDoesNotThrow(() -> g2.addAnyVariable(start)); + + assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(nullTerm)); + assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(nts)); + + d_solver.synthFun("f", new Term[] {}, bool, g1); + + assertThrows(CVC5ApiException.class, () -> g1.addAnyVariable(start)); + } +} |