summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-07-26Initial work on PreprocessingPassRegistryrefactor_pp_registryAndres Noetzli
2017-07-26commented out SimplifyAssertions Pass, will refactor in the futureJustin Xu
2017-07-24rebasedJustin Xu
2017-07-24rebasedJustin Xu
2017-07-24CNFPass and RemoveITE and TheoryPreprocessJustin Xu
2017-07-24ContrainSubtypes and ExpandingDefinitions classesJustin Xu
2017-07-24Changed return type and added friend classes to fix bugs on a few classes.Justin Xu
2017-07-24StaticLearningPass added friend but one test case is brokenJustin Xu
2017-07-24Finished implementing pbRewrites, RewriteApplyToConst, BitBlastEager, and ↵Justin Xu
NoConflict classes. isQuantified, StaticLearning, and RepeatSimp still commented out, unsure how to implement function calls
2017-07-24QuantifiedPass bugged,commented outJustin Xu
2017-07-24Fixed bugs for tests up to isQuantified flagJustin Xu
2017-07-24added QuantifiedPass classjustinxu421
2017-07-24added CEguided, BitBlast, BVAbstraction, UnconstrainedSimp, Rewrite, ↵justinxu421
NotUnsatCores, SepPreSkolemPass classes
2017-07-24refactored 'real as ints' 'ints as bv', 'bvToBool', and 'Booltobv' in the ↵justinxu421
preprocessing step
2017-07-24Example for refactoringAndres Notzli
2017-07-24CNFPass and RemoveITE and TheoryPreprocessJustin Xu
2017-07-24ContrainSubtypes and ExpandingDefinitions classesJustin Xu
2017-07-23Disabling compiling unit tests with coverity scan for now.Tim King
2017-07-22Deprecating the unused convenience_node_builders.h (#203)Tim King
2017-07-22Consolidating the opaque pointers in SymbolTable. (#204)Tim King
* Consolidating the opaque pointers in SymbolTable. This removes details about the implementation from a public header. * Removing the guard for SymbolTable for the move constructor.
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
* Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes.
2017-07-20Changed return type and added friend classes to fix bugs on a few classes.Justin Xu
2017-07-20Fix a few bugs related to sygus.ajreynol
2017-07-19Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. ↵Tim King
Removing it as well.
2017-07-19Fix simple_vc_compat_cxx example (#202)Andres Noetzli
The CVC3 compatibility layer was broken because it was setting simplification mode to SIMPLIFICATION_MODE_INCREMENTAL, which is not supported anymore since commit 2dbe1f150d30f0fb0c8522f891104270ce09db4c . This commit changes the compatibility layer to not set the option anymore. This addresses bug 833, which had been reported on the cvc-bugs mailing list.
2017-07-18Adding a garbage list that get collected during the ~Scope. Removing the ↵Tim King
CDHashMap garbage.
2017-07-17StaticLearningPass added friend but one test case is brokenJustin Xu
2017-07-17Use is_sorted, merge, copy from std (#199)Andres Noetzli
Previously, we were checking whether we should use is_sorted from std or __gnu_cxx. With C++11, std::is_sorted is guaranteed to exist. This commit changes arith/normal_form.{h,cpp} to always use std::is_sorted and also removes the custom implementations for merge and copy by using the std implementations instead.
2017-07-17Remove PtrCloser (#198)Andres Noetzli
With C++11, we don't need PtrCloser anymore because we can just use std::unique_ptr.
2017-07-16Moving to static_assert now that c++11 is available.Tim King
2017-07-16Use CXXFLAGS when compiling parsers (#197)Andres Noetzli
ANTLR generates C files that we compile with the C++ compiler. To do so, we set CC=CXX in the `Makefile.am`s of the parsers. Previously, we did not copy the CXXFLAGS to the CFLAGS, which could result in problems, e.g. when using -std=gnu++11 in the CXXFLAGS, compiling the parsers would fail if they used C++11 features (configure.ac usually modifies CXX to include the -std=gnu++11 flag but if it is included in CXXFLAGS, the CXX is not changed).
2017-07-15Fix warning about unknown escape sequence (#196)Andres Noetzli
2017-07-14Disable separate gnu++11 tests on Travis (#193)Andres Noetzli
Given that we are now always compiling with gnu++11, we don't need separate tests anymore.
2017-07-14Finished implementing pbRewrites, RewriteApplyToConst, BitBlastEager, and ↵Justin Xu
NoConflict classes. isQuantified, StaticLearning, and RepeatSimp still commented out, unsure how to implement function calls
2017-07-14Removing BOOST_FOREACH usage.Tim King
2017-07-13Merge pull request #188 from aniemetz/cx11Aina Niemetz
autoconf: make -std=gnu++11 mandatory
2017-07-13autoconf: make -std=gnu++11 mandatoryAina Niemetz
2017-07-12QuantifiedPass bugged,commented outJustin Xu
2017-07-12Fixed bugs for tests up to isQuantified flagJustin Xu
2017-07-12Fix unit tests for subranges. Fix destructors for context objs in unit tests.ajreynol
2017-07-12Fix .i files from last commit.ajreynol
2017-07-12Make type rules more strict for operators whose type rules involve subtypes. ↵ajreynol
Disable support for subrange and predicate subtypes (which were only partially supported previously).
2017-07-11Remove trailing slashes from directories if specified via command line.Mathias Preiner
2017-07-10Do not exit when value/model/unsat-core/proof is requested at wrong time, ↵ajreynol
for bug 831.
2017-07-10Add nl regression.ajreynol
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring ↵ajreynol
of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
2017-07-10Separate sygus term utilities to new file, minor cleanup from last commit.ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵ajreynol
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
2017-07-10Prerelease versioning for master.Mathias Preiner
2017-07-10Cutting release 1.5.Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback