| summaryrefslogtreecommitdiff |
diff options
| author | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-07-31 15:05:30 +0200 |
|---|---|---|
| committer | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-07-31 15:05:30 +0200 |
| commit | 067f596822b80b2786ce2bb895a593d479516cad (patch) | |
| tree | 52c7fed0824edd09545f9577e5f08f206ee7b628 /instr-to-kodkod/src/Main.java | |
| parent | 05fbf26dbb1b1f19e3ef76a0d0789806fa7be12c (diff) | |
First shot at the handling of regular expressions.
Diffstat (limited to 'instr-to-kodkod/src/Main.java')
| -rw-r--r-- | instr-to-kodkod/src/Main.java | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java index 6a2445b..11a357a 100644 --- a/instr-to-kodkod/src/Main.java +++ b/instr-to-kodkod/src/Main.java @@ -10,6 +10,7 @@ import kodkod.ast.Formula; import kodkod.engine.Solution; import kodkod.engine.Solver; +import kodkod.engine.config.ConsoleReporter; import kodkod.engine.satlab.SATFactory; import kodkod.instance.Bounds; @@ -337,7 +338,14 @@ public class Main return; } - /* 6/ Add all types and used predicates to the Universe. */ + /* 6/ Handle regexps */ + STRING_MANAGER.populate_regex_predicate + ( + MODEL.get_predicate("string_matches") + ); + + + /* 7/ Add all types and used predicates to the Universe. */ univ = new Universe(MODEL.get_atoms()); tf = univ.factory(); bounds = new Bounds(univ); @@ -348,7 +356,11 @@ public class Main solver = new Solver(); solver.options().setSkolemDepth(-1); solver.options().setSolver(SATFactory.DefaultSAT4J); -// solver.options().setReporter(new ConsoleReporter()); + + if (PARAMETERS.be_verbose()) + { + solver.options().setReporter(new ConsoleReporter()); + } solutions = solver.solveAll |


