cvc5.git
2020-08-11 Andrew ReynoldsRemove instantiation model true option (#4861)
2020-08-11 Aina NiemetzNew C++ API: Remove redundant API functions for mkReal...
2020-08-09 Andrew ReynoldsMake valuation class more robust to null underlying...
2020-08-09 Andrew ReynoldsSplitting a few utility classes from EqualityEngine...
2020-08-08 Andrew ReynoldsMove datatype index constant to its own file (#4859)
2020-08-07 Aina NiemetzGH Actions: Remove cancel action. (#4843)
2020-08-06 Andrew ReynoldsUpdates not related to creation for eliminating Expr...
2020-08-06 Andrew ReynoldsSplit preprocessor from SmtEngine (#4854)
2020-08-06 Andrew Reynolds(proof-new) Refactor regular expression operation ...
2020-08-05 Andrew ReynoldsSplit Assertions from SmtEngine (#4788)
2020-08-05 Gereon KremerImprove error message for unsupported exponents (#4852)
2020-08-05 Andrew V. JonesWhen checking models, ensure that error message is...
2020-08-05 Andres Noetzli[Strings] Add eager context-dependent evaluation (...
2020-08-05 Gereon KremerAdd dummy returns if libpoly is unavailable. (#4845)
2020-08-04 Andrew ReynoldsFixes for getInterpolant and getAbduct API methods...
2020-08-04 Mathias PreinerAdd documentation and build instructions for recompilat...
2020-08-04 Abdalrhman... Modify the smt2 parser to use the Sygus grammar. (...
2020-08-04 Andrew ReynoldsAdd API interface for specialized constructor term...
2020-08-04 Gereon KremerProperly initialize d_fullyInited. (#4840)
2020-08-04 Gereon KremerAdd CAD-based solver (#4834)
2020-08-03 Andres NoetzliUpdate documentation for Solver::mkVar() (#4833)
2020-08-03 Ying ShengAdd implementation for SyGuS interpolation module ...
2020-08-03 yoni206New BV rewrite rules aimed at bv_to_int preprocessing...
2020-08-03 Andrew ReynoldsGeneralize interface for candidate rewrite database...
2020-08-03 Andrew ReynoldsUpdate datatypes in cvc parser to the new API (#4826)
2020-08-03 yoni206Examples for using sygus python api (#4822)
2020-08-03 makaimannDelete solver pointer in Cython __dealloc__ (#4799)
2020-08-03 Andrew ReynoldsSplit expression names from SmtEngine (#4832)
2020-08-03 Andrew ReynoldsSplit dump manager from SmtEngine (#4824)
2020-08-02 Andrew ReynoldsUpdates to dtype constructor in preparation for elimina...
2020-08-02 Andres NoetzliFix ASan failure in interactive_shell_black (#4827)
2020-08-02 Andres NoetzliEnsure strict length constraint for decompose rule...
2020-08-02 Andrew ReynoldsAdd methods for constructing datatype types from NodeMa...
2020-08-01 Andrew V. JonesEnsure that we only find '.a's when building statically...
2020-08-01 Andrew ReynoldsFix component contains for splicing due to substring...
2020-08-01 yoni206Add SyGuS Python API (#4812)
2020-07-31 Andrew ReynoldsSplit listener classes from SmtEngine (#4816)
2020-07-31 Andrew ReynoldsStandardize explanations in arrays (#4804)
2020-07-30 Andres NoetzliPython API: Add support for sequences (#4757)
2020-07-30 Gereon KremerCad implementation (#4774)
2020-07-30 Gereon KremerAdds the interface for the CAD-based arithmetic solver...
2020-07-30 Andrew V. JonesWhen linking Editline, use 'pkg-config' to correctly...
2020-07-30 Andrew ReynoldsFix null case for sygus printing (#4793)
2020-07-30 Andrew Reynolds(proof-new) Stream output for ProofNode (#4789)
2020-07-30 Andrew Reynolds(proof-new) Fixes for getFreeAssumptions (#4802)
2020-07-28 Ying Shengfixing issue #4808. (#4810)
2020-07-28 Andrew ReynoldsRemove arrays lazy rintro option (#4806)
2020-07-28 Andres NoetzliReplace Expr with Node in Term/Op (#4781)
2020-07-28 Andrew ReynoldsFix regular expression delta for complement (#4765)
2020-07-28 yoni206Supporting seq.nth (#4723)
2020-07-28 Ying ShengInterpolation: Add interface for SyGuS interpolation...
2020-07-28 Andrew ReynoldsUse lemma property enum for OutputChannel::lemma (...
2020-07-27 Andrew Reynolds(proof-new) Proof production for term formula removal...
2020-07-27 Andrew Reynolds(proof-new) Arithmetic operator elim proof producing...
2020-07-27 Alex OzdemirConsider negation's proof before triggering arith pfs...
2020-07-21 Aina NiemetzGH Actions: Cancel builds on push, remove redundant...
2020-07-21 Andrew ReynoldsSupport uninterpreted constants in the evaluator (...
2020-07-21 Gereon KremerPreparations for a CAD-based arithmetic solver (#4762)
2020-07-20 Alex OzdemirFix a deadlock in the signature tests. (#4772)
2020-07-18 Haniel BarbosaImproving equality engine tracing (#4770)
2020-07-18 Andrew Reynolds(proof-new) Proof recording for assertions pipeline...
2020-07-18 Andrew ReynoldsEnumerate shapes feature in fast sygus enumerator ...
2020-07-17 Andres NoetzliAdd NodeManagerScopes to fix use-after-free issues...
2020-07-17 Andrew ReynoldsReplace options listener infrastructure (#4764)
2020-07-17 Andrew V. JonesSupport for using 'libedit' over 'readline' #4571 ...
2020-07-17 Andrew Reynolds(proof-new) Updates to strings core solver (#4642)
2020-07-17 Andrew ReynoldsAdd option manager and simpler option listener (#4745)
2020-07-17 Gereon KremerIntegration of libpoly (#4679)
2020-07-17 Haniel BarbosaFix EqProof to ProofNode conversion (#4760)
2020-07-16 Haniel Barbosa(proof-new) Implements the conversion between EqProof...
2020-07-16 Gereon KremerResource manager cleanup (#4732)
2020-07-16 Andrew ReynoldsSplit abstract values utility from SmtEngine (#4754)
2020-07-16 Andrew ReynoldsMake ExtTheory a utility and not a member of Theory...
2020-07-16 Gereon KremerRemove cumulative time limits and cpu time limits ...
2020-07-16 Gereon KremerFixes memory leak when an exception goes through runCvc...
2020-07-16 Haniel Barbosa(proof-new) Adding API for converting EqProof into...
2020-07-15 Andres NoetzliUse Nodes for SmtEngine assertions (#4752)
2020-07-15 Andrew ReynoldsSplit abduction solver from SmtEngine (#4733)
2020-07-15 Andres NoetzliUse TypeNode in UninterpretedConstant (#4748)
2020-07-15 Gereon KremerAdd missing header (Fixes #4743) (#4749)
2020-07-15 Andrew ReynoldsSimplify entailment check interface (#4744)
2020-07-14 Andrew ReynoldsMake use of options in setDefaults more consistent...
2020-07-14 Andrew ReynoldsRemove sygus print callback (#4727)
2020-07-14 Andrew ReynoldsFix regression output. (#4741)
2020-07-14 Andrew Reynolds(proof-new) Skeleton proof support in the Rewriter...
2020-07-14 Andres NoetzliUse TypeNode in EmptySet (#4740)
2020-07-14 Andrew ReynoldsDebug instantiations output (#4739)
2020-07-14 Andrew ReynoldsMinor refactoring of subsolver initialization (#4731)
2020-07-14 Andres NoetzliFix caching in TheoryEngine::getExplanation() (#4736)
2020-07-14 Haniel BarbosaFix options messages that were inverted (#4734)
2020-07-14 Andres NoetzliUse TypeNode/Node in ArrayStoreAll (#4728)
2020-07-14 Andrew ReynoldsFix type comparisons involving pointer. (#4738)
2020-07-14 Andrew ReynoldsFix whitespace issue in instantiations output. (#4737)
2020-07-13 Andrew Reynolds (proof-new) SMT Preprocess proof generator (#4708)
2020-07-13 Andrew Reynolds User-facing print debug option for sygus candidates...
2020-07-13 Andrew ReynoldsStatistics on instantiations per quantified formula...
2020-07-13 Gereon KremerImplement --tlimit for windows (#4716)
2020-07-13 Andrew ReynoldsAdd support for string/sequence update (#4725)
2020-07-13 Andres NoetzliRemove ExprSequence (#4724)
2020-07-11 Andrew ReynoldsCache explanations in TheoryEngine::getExplanation...
next