cvc5.git
8 years agomore code refactor
PaulMeng [Sun, 24 Jul 2016 23:58:22 +0000 (19:58 -0400)]
more code refactor

8 years agomore code refactor
Paul Meng [Sun, 24 Jul 2016 20:31:57 +0000 (16:31 -0400)]
more code refactor

8 years agorefactored code
Paul Meng [Sat, 23 Jul 2016 20:35:51 +0000 (16:35 -0400)]
refactored code

8 years agobug fixes for reachablity check
PaulMeng [Wed, 20 Jul 2016 20:04:24 +0000 (16:04 -0400)]
bug fixes for reachablity check

8 years agoadded support for expansion of transitive closure
Paul Meng [Tue, 12 Jul 2016 01:40:25 +0000 (21:40 -0400)]
added support for expansion of transitive closure

8 years agoresolved merge conflicts
PaulMeng [Tue, 5 Jul 2016 18:21:11 +0000 (14:21 -0400)]
resolved merge conflicts

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4.git
PaulMeng [Tue, 5 Jul 2016 17:56:53 +0000 (13:56 -0400)]
Merge branch 'master' of https://github.com/CVC4/CVC4.git

Conflicts:
proofs/signatures/Makefile.am
src/Makefile.am
src/expr/datatype.cpp
src/options/datatypes_options
src/options/options_template.cpp
src/options/quantifiers_options
src/proof/arith_proof.cpp
src/proof/arith_proof.h
src/proof/array_proof.cpp
src/proof/array_proof.h
src/proof/bitvector_proof.cpp
src/proof/bitvector_proof.h
src/proof/cnf_proof.cpp
src/proof/cnf_proof.h
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/sat_proof.h
src/proof/sat_proof_implementation.h
src/proof/skolemization_manager.h
src/proof/theory_proof.cpp
src/proof/theory_proof.h
src/proof/uf_proof.cpp
src/proof/uf_proof.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine_check_proof.cpp
src/theory/arrays/array_proof_reconstruction.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/candidate_generator.h
src/theory/quantifiers/ce_guided_single_inv.cpp
src/theory/quantifiers/ceg_instantiator.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/equality_infer.cpp
src/theory/quantifiers/equality_infer.h
src/theory/quantifiers/inst_match_generator.cpp
src/theory/quantifiers/inst_propagator.cpp
src/theory/quantifiers/inst_propagator.h
src/theory/quantifiers/inst_strategy_e_matching.cpp
src/theory/quantifiers/inst_strategy_e_matching.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h
src/theory/quantifiers/quant_split.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers/trigger.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/sets/kinds
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_rules.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/strings/Makefile.am
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/max2-univ.sy

8 years agofixes bugs in std effort for TC
PaulMeng [Tue, 5 Jul 2016 15:56:31 +0000 (11:56 -0400)]
fixes bugs in std effort for TC

8 years agoWhen proving a lemma, ignore literals that don't belong to the theory in question...
Guy [Fri, 1 Jul 2016 23:49:02 +0000 (16:49 -0700)]
When proving a lemma, ignore literals that don't belong to the theory in question, except for equalties

8 years agoHandle bitvector lemmas where a literal gets rewritten into false, and consequently...
Guy [Fri, 1 Jul 2016 21:21:13 +0000 (14:21 -0700)]
Handle bitvector lemmas where a literal gets rewritten into false, and consequently the lemma doesn't match a recorded conflict

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Thu, 30 Jun 2016 19:39:01 +0000 (12:39 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoSupport for the letification of chained AND and OR operations in LFSC proofs
Guy [Thu, 30 Jun 2016 19:38:56 +0000 (12:38 -0700)]
Support for the letification of chained AND and OR operations in LFSC proofs

8 years agodebug statement
PaulMeng [Sat, 25 Jun 2016 22:25:59 +0000 (18:25 -0400)]
debug statement

8 years agoMerge remote-tracking branch 'origin/master'
PaulMeng [Sat, 25 Jun 2016 22:20:30 +0000 (18:20 -0400)]
Merge remote-tracking branch 'origin/master'

8 years agotest
PaulMeng [Sat, 25 Jun 2016 21:55:09 +0000 (17:55 -0400)]
test

8 years agoreimplemented std effort for TC
PaulMeng [Sat, 25 Jun 2016 21:55:09 +0000 (17:55 -0400)]
reimplemented std effort for TC

8 years agoAdd theory/sep/kinds to EXTRA_DIST to fix distcheck failures.
Clark Barrett [Thu, 23 Jun 2016 23:56:49 +0000 (16:56 -0700)]
Add theory/sep/kinds to EXTRA_DIST to fix distcheck failures.

8 years agoFixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,
Clark Barrett [Thu, 23 Jun 2016 23:55:09 +0000 (16:55 -0700)]
Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,
re-enabled cdmap_black.

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Mon, 20 Jun 2016 21:20:30 +0000 (14:20 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoAddressed a bug that occurs when proof production is triggered via text flags in...
Guy [Mon, 20 Jun 2016 21:20:15 +0000 (14:20 -0700)]
Addressed a bug that occurs when proof production is triggered via text flags in the input.
Separated some initialization into two phases:
1. Those that can be done when the proof compiliation flag is set
2. Those that can be done only when the --proof option is set.
For #2, deferred their execution until the text flags in the input have been processed

8 years agoMinor change to sep/kinds
ajreynol [Mon, 20 Jun 2016 17:47:04 +0000 (12:47 -0500)]
Minor change to sep/kinds

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Mon, 20 Jun 2016 17:17:04 +0000 (10:17 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoFixed a bug where the proofManager's init() call was not getting called, resutling...
Guy [Mon, 20 Jun 2016 12:40:20 +0000 (05:40 -0700)]
Fixed a bug where the proofManager's init() call was not getting called, resutling a null point deference

8 years agoFix unit test.
ajreynol [Sat, 18 Jun 2016 15:49:21 +0000 (10:49 -0500)]
Fix unit test.

8 years agoCleanup from last commit, treat sep.nil as variable kind.
ajreynol [Fri, 17 Jun 2016 23:38:16 +0000 (18:38 -0500)]
Cleanup from last commit, treat sep.nil as variable kind.

8 years agoSupport for separation logic. Enable cbqi by default for pure BV.
ajreynol [Fri, 17 Jun 2016 20:55:56 +0000 (15:55 -0500)]
Support for separation logic. Enable cbqi by default for pure BV.

8 years agoAdd syguscomp2016 scripts.
ajreynol [Fri, 17 Jun 2016 14:22:09 +0000 (09:22 -0500)]
Add syguscomp2016 scripts.

8 years agoDummy commit.
Clark Barrett [Thu, 9 Jun 2016 18:04:41 +0000 (11:04 -0700)]
Dummy commit.

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Guy [Wed, 8 Jun 2016 22:24:44 +0000 (15:24 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoLFSC letification is true by default
Guy [Wed, 8 Jun 2016 18:53:02 +0000 (11:53 -0700)]
LFSC letification is true by default

8 years agoSupport for printing a global let map in LFSC proofs.
Guy [Wed, 8 Jun 2016 18:52:42 +0000 (11:52 -0700)]
Support for printing a global let map in LFSC proofs.
Added a flag to enable/disbale this feature (enabled by default).

Also, added some infrastructure for proving rewrite rules.

8 years agoMerge pull request #85 from CVC4/master_for_proof_merge
guykatzz [Mon, 6 Jun 2016 17:48:50 +0000 (10:48 -0700)]
Merge pull request #85 from CVC4/master_for_proof_merge

Merge from proof branch

8 years agoRemove NodeListMap from datatypes and equality inference. Add option --dt-blast-splits.
ajreynol [Sat, 4 Jun 2016 00:07:05 +0000 (19:07 -0500)]
Remove NodeListMap from datatypes and equality inference. Add option --dt-blast-splits.

8 years agoBetter infrastructure for proving constant disequality.
Guy [Fri, 3 Jun 2016 21:27:00 +0000 (14:27 -0700)]
Better infrastructure for proving constant disequality.
Added support for the BV case

8 years agoA better mechanism for handling BV terms with aliases: inject the alias at the decl_b...
Guy [Fri, 3 Jun 2016 21:10:42 +0000 (14:10 -0700)]
A better mechanism for handling BV terms with aliases: inject the alias at the decl_bblast step, instead of having an individual "with alias" rule for each BV operation

8 years agoRemove NodeListMap from strings, fixes memory leaks. Fix for regexp intersection.
ajreynol [Fri, 3 Jun 2016 19:20:55 +0000 (14:20 -0500)]
Remove NodeListMap from strings, fixes memory leaks. Fix for regexp intersection.

8 years agoSimple memory fixes, minor cleanup in quantifiers.
ajreynol [Fri, 3 Jun 2016 16:39:12 +0000 (11:39 -0500)]
Simple memory fixes, minor cleanup in quantifiers.

8 years agoReduce number of passes in quantifiers rewriter.
ajreynol [Fri, 3 Jun 2016 14:01:30 +0000 (09:01 -0500)]
Reduce number of passes in quantifiers rewriter.

8 years agoFixed a magical bug that only appears when compiling with clang:
Guy [Thu, 2 Jun 2016 21:44:58 +0000 (14:44 -0700)]
Fixed a magical bug that only appears when compiling with clang:
The assignment
      d_exprToVariableName[*it] = assignAlias(*it)

Creates an empty value for *it in d_exprToVariableName, causing the assertion in assignAlias to fail

8 years agoFix
Guy [Thu, 2 Jun 2016 17:17:14 +0000 (10:17 -0700)]
Fix

8 years agoMerge from proof branch
Guy [Thu, 2 Jun 2016 00:46:24 +0000 (17:46 -0700)]
Merge from proof branch

8 years agoRevert "Merging proof branch"
Guy [Thu, 2 Jun 2016 00:41:17 +0000 (17:41 -0700)]
Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

8 years agoMerging proof branch
Guy [Thu, 2 Jun 2016 00:33:41 +0000 (17:33 -0700)]
Merging proof branch

8 years agoFix to ignore a case of triggers with no free variables.
ajreynol [Wed, 1 Jun 2016 21:25:50 +0000 (16:25 -0500)]
Fix to ignore a case of triggers with no free variables.

8 years agoInitial infrastructure for bounded set quantification (disabled). Refactoring and...
ajreynol [Wed, 1 Jun 2016 20:51:39 +0000 (15:51 -0500)]
Initial infrastructure for bounded set quantification (disabled). Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers.

8 years agoAdded Guy to authors list.
Clark Barrett [Tue, 31 May 2016 01:01:14 +0000 (18:01 -0700)]
Added Guy to authors list.

8 years agoFix build
Clark Barrett [Sat, 28 May 2016 17:52:38 +0000 (10:52 -0700)]
Fix build

8 years agoUpdated incremental run script
Clark Barrett [Sat, 28 May 2016 17:28:38 +0000 (10:28 -0700)]
Updated incremental run script

8 years agoDisabling failing unit test for now
Clark Barrett [Sat, 28 May 2016 15:58:44 +0000 (08:58 -0700)]
Disabling failing unit test for now

8 years agoRemoving check that is no longer valid.
Clark Barrett [Sat, 28 May 2016 00:43:40 +0000 (17:43 -0700)]
Removing check that is no longer valid.

8 years agoMerged QF_UFBV support from experimental branch
Clark Barrett [Fri, 27 May 2016 21:40:20 +0000 (14:40 -0700)]
Merged QF_UFBV support from experimental branch

8 years agoEnabled bit-blasting option for QF_UFBV
Clark Barrett [Fri, 27 May 2016 21:28:24 +0000 (14:28 -0700)]
Enabled bit-blasting option for QF_UFBV

8 years agoUpdated incremental script
Clark Barrett [Fri, 27 May 2016 06:26:12 +0000 (23:26 -0700)]
Updated incremental script

8 years agoFixed bug in run script
Clark Barrett [Fri, 27 May 2016 04:03:39 +0000 (21:03 -0700)]
Fixed bug in run script

8 years agoAdded cryptominisat flag to QF_NIA
Kshitij Bansal [Thu, 26 May 2016 23:18:59 +0000 (19:18 -0400)]
Added cryptominisat flag to QF_NIA

8 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Clark Barrett [Thu, 26 May 2016 23:15:16 +0000 (16:15 -0700)]
Merge branch 'master' of https://github.com/CVC4/CVC4

8 years agoSmall change in run script
Clark Barrett [Thu, 26 May 2016 23:12:14 +0000 (16:12 -0700)]
Small change in run script

8 years agoChanged aig_bitblaster to work with cryptominisat
lianah [Thu, 26 May 2016 23:05:01 +0000 (19:05 -0400)]
Changed aig_bitblaster to work with cryptominisat

8 years agoDisabled m4ri in cryptominisat cmake command
lianah [Thu, 26 May 2016 22:35:34 +0000 (18:35 -0400)]
Disabled m4ri in cryptominisat cmake command

8 years agoFix for aig_bitblaster.cpp
Kshitij Bansal [Thu, 26 May 2016 22:19:51 +0000 (18:19 -0400)]
Fix for aig_bitblaster.cpp

8 years agoUse term indexing in TheoryUF::computeCareGraph. Do not reject model value instantiat...
ajreynol [Thu, 26 May 2016 19:51:01 +0000 (14:51 -0500)]
Use term indexing in TheoryUF::computeCareGraph. Do not reject model value instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.

8 years agoUpdated script, fixed bug in QF_NIA conversion.
Clark Barrett [Thu, 26 May 2016 19:41:05 +0000 (12:41 -0700)]
Updated script, fixed bug in QF_NIA conversion.

8 years agoFixed unit test
Liana Hadarean [Wed, 25 May 2016 07:03:53 +0000 (00:03 -0700)]
Fixed unit test

8 years agoFixed build issue due to dummy Cryptominisat constructor.
Liana Hadarean [Wed, 25 May 2016 06:16:06 +0000 (23:16 -0700)]
Fixed build issue due to dummy Cryptominisat constructor.

8 years agoForgot to add second patch file.
Liana Hadarean [Wed, 25 May 2016 05:36:14 +0000 (22:36 -0700)]
Forgot to add second patch file.

8 years agoMerged cryptominisat from experimental branch.
Liana Hadarean [Wed, 25 May 2016 05:30:41 +0000 (22:30 -0700)]
Merged cryptominisat from experimental branch.

8 years agoImprovements to symmetry breaking in sygus search. Minor fix for getting instantiatio...
ajreynol [Tue, 24 May 2016 23:18:00 +0000 (18:18 -0500)]
Improvements to symmetry breaking in sygus search. Minor fix for getting instantiations of non-registered quantifiers in sygus.

8 years agoFix related to parametric sorts whose interpretation is finite due to uninterpreted...
ajreynol [Mon, 23 May 2016 19:28:29 +0000 (14:28 -0500)]
Fix related to parametric sorts whose interpretation is finite due to uninterpreted sorts + FMF.  Generalizes previous fix in term registration visitor.

8 years agoMinor fix for strings.
ajreynol [Sat, 21 May 2016 21:58:19 +0000 (16:58 -0500)]
Minor fix for strings.

8 years agoMinor fix to strings, cleanup in datatypes.
ajreynol [Fri, 20 May 2016 22:10:03 +0000 (17:10 -0500)]
Minor fix to strings, cleanup in datatypes.

8 years agoImprovements to theory combination + strings: do not return trivial care graph, split...
ajreynol [Fri, 20 May 2016 18:59:13 +0000 (13:59 -0500)]
Improvements to theory combination + strings: do not return trivial care graph, split on length terms for disequal strings. Term indexing for TheoryDatatypes::computeCareGraph. Minor fix in quantifiers rewriter for entailed conditions, strings cardinality.

8 years agoUpdated AUTHORS file
Clark Barrett [Fri, 20 May 2016 12:58:06 +0000 (05:58 -0700)]
Updated AUTHORS file

8 years agoRefactor modes for sygus+single invocation. Add option --inst-rlv-cond. Minor fixes...
ajreynol [Wed, 18 May 2016 15:06:49 +0000 (10:06 -0500)]
Refactor modes for sygus+single invocation.  Add option --inst-rlv-cond. Minor fixes for inst max level.

8 years agoMinor fix cbqi for constant monomials.
ajreynol [Tue, 17 May 2016 17:52:44 +0000 (12:52 -0500)]
Minor fix cbqi for constant monomials.

8 years agoFix memory leak in interactive_shell.cpp
Clark Barrett [Mon, 16 May 2016 20:27:57 +0000 (13:27 -0700)]
Fix memory leak in interactive_shell.cpp

8 years agoEnable --sygus-direct-eval by default, limit to terms that do not induce Boolean...
ajreynol [Mon, 16 May 2016 22:30:59 +0000 (17:30 -0500)]
Enable --sygus-direct-eval by default, limit to terms that do not induce Boolean structure.  Minor fixes for bitvectors: rewrite SDIV to total operators when options::bitvectorDivByZeroConst is true, fix collectModelInfo when fullModel=false. Lift ITEs in sygus search. Fix sygus initialization related to cbqi.

8 years agoWork on --sygus-direct-eval. Minor optimizations, updates to casc scripts. Enable...
ajreynol [Sun, 15 May 2016 17:34:51 +0000 (12:34 -0500)]
Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. Enable e-matching when --strings-exp is enabled.

8 years agoAdd casc scripts. Improvements to qcf related to nested quantifiers and variable...
ajreynol [Thu, 12 May 2016 15:13:17 +0000 (10:13 -0500)]
Add casc scripts. Improvements to qcf related to nested quantifiers and variable ordering.

8 years agoFix for --inst-max-level
ajreynol [Tue, 10 May 2016 20:10:10 +0000 (15:10 -0500)]
Fix for --inst-max-level

8 years agoAdd smt comp 2016 scripts. Fix for --relevant-triggers. Add minor optimizations to...
ajreynol [Tue, 10 May 2016 19:33:08 +0000 (14:33 -0500)]
Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor optimizations to sygus and qcf.

8 years agoRe-enabling ite simplification in incremental mode - no reason why
Clark Barrett [Mon, 9 May 2016 22:21:22 +0000 (15:21 -0700)]
Re-enabling ite simplification in incremental mode - no reason why
it should be a problem.

8 years agoMinor clean up, fixes related to sygus.
ajreynol [Fri, 6 May 2016 22:04:52 +0000 (17:04 -0500)]
Minor clean up, fixes related to sygus.

8 years agoCompute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant...
ajreynol [Thu, 5 May 2016 23:44:47 +0000 (18:44 -0500)]
Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges.  Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.

8 years agochange to use tuple element representatives to build TC graph for full
PaulMeng [Thu, 5 May 2016 19:58:10 +0000 (14:58 -0500)]
change to use tuple element representatives to build TC graph for full
effort

8 years agoRemoving a null pointer reference that was found by -fsanitize=null.
Tim King [Thu, 5 May 2016 17:35:04 +0000 (10:35 -0700)]
Removing a null pointer reference that was found by -fsanitize=null.

8 years agoUpdate to COPYING
Clark Barrett [Thu, 5 May 2016 04:30:13 +0000 (21:30 -0700)]
Update to COPYING

8 years agoimplemented TC for standard effort
PaulMeng [Wed, 4 May 2016 15:21:18 +0000 (10:21 -0500)]
implemented TC for standard effort

8 years agoClean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not...
ajreynol [Mon, 2 May 2016 14:16:30 +0000 (09:16 -0500)]
Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.

8 years agoReviewed Tim's Asan changes and improved SatProof comments.
Liana Hadarean [Sat, 30 Apr 2016 16:57:43 +0000 (09:57 -0700)]
Reviewed Tim's Asan changes and improved SatProof comments.

8 years agoWorkaround for a problem in clang
Clark Barrett [Thu, 28 Apr 2016 21:39:35 +0000 (17:39 -0400)]
Workaround for a problem in clang

8 years agoMore work on inst propagate. Optimization for qcf to check instances eagerly. Improv...
ajreynol [Thu, 28 Apr 2016 12:01:05 +0000 (07:01 -0500)]
More work on inst propagate.  Optimization for qcf to check instances eagerly. Improvements to equality query for disequalities.

8 years agoAdding an example lsan supression file.
Tim King [Wed, 27 Apr 2016 19:54:29 +0000 (12:54 -0700)]
Adding an example lsan supression file.

8 years agoFixing memory leaks for garbage collection of ResChains in the sat proof implementati...
Tim King [Tue, 26 Apr 2016 21:51:04 +0000 (14:51 -0700)]
Fixing memory leaks for garbage collection of ResChains in the sat proof implementation. As a part of tracking this down, I've modified a number of accessor functions in TSatProof to be const. An expert in this code will need to do a pass over this.

8 years agoFixing a memory leak of the ProofManager.
Tim King [Tue, 26 Apr 2016 17:52:15 +0000 (10:52 -0700)]
Fixing a memory leak of the ProofManager.

8 years agoupdate from the master
PaulMeng [Wed, 20 Apr 2016 19:43:18 +0000 (14:43 -0500)]
update from the master

8 years agoadd utils class for relational theory
PaulMeng [Wed, 20 Apr 2016 18:54:32 +0000 (13:54 -0500)]
add utils class for relational theory

8 years agoRefactored code
PaulMeng [Wed, 20 Apr 2016 03:51:30 +0000 (22:51 -0500)]
Refactored code

8 years agoFixed typo
Clark Barrett [Tue, 19 Apr 2016 16:01:14 +0000 (09:01 -0700)]
Fixed typo

8 years agoMore fixes for python interface
Clark Barrett [Mon, 18 Apr 2016 23:06:45 +0000 (16:06 -0700)]
More fixes for python interface

8 years agoRolling back the rewrite code
Guy [Fri, 15 Apr 2016 22:34:52 +0000 (15:34 -0700)]
Rolling back the rewrite code