mirror of
https://git.freebsd.org/ports.git
synced 2025-04-28 09:36:41 -04:00
CTL-SAT is a CTL (Computation Tree Logic) SAT solver. The user may test satisfiability of a CTL formula may by providing it as a command-line argument to the ctl-sat program, e.g.: ctl-sat "~( (A(pUq) ^ AG(q->r) ^ AG(r->EXr)) -> EFEGr )" The worst-case time complexity is O((2^n)^3) for this SAT solver, while the worst-case space complexity is O((2^n)^2). WWW: https://github.com/nicolaprezza/CTLSAT
38 lines
784 B
Text
38 lines
784 B
Text
--- Makefile.orig 2015-01-07 10:27:59 UTC
|
|
+++ Makefile
|
|
@@ -2,26 +2,15 @@
|
|
|
|
SOURCE=\
|
|
formulas/AllTomorrow.cpp \
|
|
-formulas/AllTomorrow.h \
|
|
formulas/AllUntil.cpp \
|
|
-formulas/AllUntil.h \
|
|
formulas/Atom.cpp \
|
|
-formulas/Atom.h \
|
|
formulas/Conjunction.cpp \
|
|
-formulas/Conjunction.h \
|
|
formulas/ExistsTomorrow.cpp \
|
|
-formulas/ExistsTomorrow.h \
|
|
formulas/ExistsUntil.cpp \
|
|
-formulas/ExistsUntil.h \
|
|
formulas/Formula.cpp \
|
|
-formulas/Formula.h \
|
|
formulas/Negation.cpp \
|
|
-formulas/Negation.h \
|
|
parser/CTLParser.cpp \
|
|
-parser/CTLParser.h \
|
|
tableau/Tableau.cpp \
|
|
-tableau/Tableau.h \
|
|
-common.h \
|
|
main.cpp \
|
|
|
|
|
|
@@ -33,7 +22,7 @@ all: $(BINARY)
|
|
|
|
$(BINARY): $(SOURCE)
|
|
|
|
- g++ -march=native -mtune=generic -O3 $(SOURCE) -o $(BINARY)
|
|
+ $(CXX) $(CXXFLAGS) $(SOURCE) -o $(BINARY)
|
|
|
|
clean:
|
|
|